Let x0 of type ι be given.
Apply SNoS_E2 with
ordsucc omega,
x0,
∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Apply dneg with
∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).
Apply H7.
Let x1 of type ι be given.
Apply nat_ind with
λ x2 . ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x2)))),
x1 leaving 3 subgoals.
Apply eps_0_1 with
λ x2 x3 . ∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 x3))).
Apply SNoS_ordsucc_omega_bdd_above with
x0,
∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 1))) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Apply H11 with
∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 1))).
Apply SNoS_ordsucc_omega_bdd_below with
x0,
∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 1))) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Apply H14 with
∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 1))).
Apply SNoLt_trichotomy_or_impred with
x2,
x3,
∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 1))) leaving 5 subgoals.
Apply omega_SNo with
x2.
The subproof is completed by applying H12.
Apply omega_SNo with
x3.
The subproof is completed by applying H15.
Apply L10 with
x3 leaving 3 subgoals.
Apply omega_nat_p with
x3.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply SNoLt_tra with
x0,
x2,
x3 leaving 5 subgoals.
The subproof is completed by applying H5.
Apply omega_SNo with
....