Robinson Arithmetic is order-adequate

In chapter 9, Peter Smith defines the following concept: A theory T that captures the relation ≤ is order-adequate if it satisfies the following nine properties:

• O1: T ⊢ ∀x (0 ≤ x)
• O2: For any n, T ⊢ ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n) → x ≤ n)
• O3: For any n, T ⊢ ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
• O4: For any n, if T ⊢ φ(0) and T ⊢ φ(1) and ... and T ⊢ φ(n) then T ⊢ (∀x ≤ n)φ(x)
• O5: For any n, if T ⊢ φ(0) or T ⊢ φ(1) or ... or T ⊢ φ(n) then T ⊢ (∃x ≤ n)φ(x)
• O6: For any n, T ⊢ ∀x (x ≤ n → x ≤ Sn)
• O7: For any n, T ⊢ ∀x (n ≤ x  → (n = x  ∨ Sn ≤ x))
• O8: For any n, T ⊢ ∀x (x ≤ n ∨ n ≤ x)
• O9: For any n>0, T ⊢ (∀x ≤ n-1)φ(x) → (∀x ≤ n)(x ≠ n → φ(x))

Then, we have the following theorem: