Let x0 of type ι be given.
Let x1 of type ο be given.
Apply SepE with
SNoS_ (ordsucc omega),
λ x2 . and (and (x2 = omega ⟶ ∀ x3 : ο . x3) (x2 = minus_SNo omega ⟶ ∀ x3 : ο . x3)) (∀ x3 . x3 ∈ SNoS_ omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x3 (minus_SNo x2))) (eps_ x4)) ⟶ x3 = x2),
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H3 with
x1.
Apply H4 with
(∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0) ⟶ x1.
Assume H5:
x0 = omega ⟶ ∀ x2 : ο . x2.
Apply SNoS_E2 with
ordsucc omega,
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H2.
Apply SNoLeE with
minus_SNo omega,
x0,
SNoLt (minus_SNo omega) x0 leaving 5 subgoals.
Apply SNo_minus_SNo with
omega.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying H10.
Apply mordinal_SNoLev_min_2 with
omega,
x0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
The subproof is completed by applying H13.
Apply H1 leaving 7 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
The subproof is completed by applying H2.
The subproof is completed by applying L13.
The subproof is completed by applying L12.
The subproof is completed by applying H7.
Apply SNoS_ordsucc_omega_bdd_drat_intvl with
x0 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L13.
The subproof is completed by applying L12.