Let x0 of type ι be given.

Assume H0: x0 ∈ real.

Assume H1: SNoLe 0 x0.

Apply real_E with x0, ∃ x1 . and (x1 ∈ omega) (and (SNoLe x1 x0) (SNoLt x0 (ordsucc x1))) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: SNo x0.

Assume H3: SNoLev x0 ∈ ordsucc omega.

Assume H4: x0 ∈ SNoS_ (ordsucc omega).

Assume H6: SNoLt x0 omega.

Assume H7: ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0.

Assume H8: ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).

Apply H8 with 0, ∃ x1 . and (x1 ∈ omega) (and (SNoLe x1 x0) (SNoLt x0 (ordsucc x1))) leaving 2 subgoals.

Apply nat_p_omega with 0.

The subproof is completed by applying nat_0.

Let x1 of type ι be given.

Assume H9: (λ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ 0))))) x1.

Apply H9 with ∃ x2 . and (x2 ∈ omega) (and (SNoLe x2 x0) (SNoLt x0 (ordsucc x2))).

Assume H10: x1 ∈ SNoS_ omega.

Assume H11: and (SNoLt x1 x0) (SNoLt x0 (add_SNo x1 (eps_ 0))).

Apply H11 with ∃ x2 . and (x2 ∈ omega) (and (SNoLe x2 x0) (SNoLt x0 (ordsucc x2))).

Assume H12: SNoLt x1 x0.

Apply eps_0_1 with λ x2 x3 . SNoLt x0 (add_SNo x1 x3) ⟶ ∃ x4 . and (x4 ∈ omega) (and (SNoLe x4 x0) (SNoLt x0 (ordsucc x4))).

Assume H13: SNoLt x0 (add_SNo x1 1).

Apply SNoS_E with omega, x1, ∃ x2 . and (x2 ∈ omega) (and (SNoLe x2 x0) (SNoLt x0 (ordsucc x2))) leaving 3 subgoals.

The subproof is completed by applying omega_ordinal.

The subproof is completed by applying H10.

Let x2 of type ι be given.

Assume H14: (λ x3 . and (x3 ∈ omega) (SNo_ x3 x1)) x2.

Apply H14 with ∃ x3 . and (x3 ∈ omega) (and (SNoLe x3 x0) (SNoLt x0 (ordsucc x3))).

Assume H15: x2 ∈ omega.

Assume H16: SNo_ x2 x1.

Claim L17: ...

...

Apply nat_ind with λ x3 . SNoLt x0 x3 ⟶ ∃ x4 . and (x4 ∈ omega) (and (SNoLe x4 x0) (SNoLt x0 (ordsucc x4))), ordsucc x2 leaving 4 subgoals.

Assume H18: SNoLt x0 0.

Apply FalseE with ∃ x3 . and (x3 ∈ omega) (and (SNoLe x3 ...) ...).

...

■

Proofgold Proof