Let x0 of type ι be given.

Assume H0: x0 ∈ real.

Let x1 of type ο be given.

Assume H1: ∀ x2 . x2 ∈ setexp (SNoS_ omega) omega ⟶ ∀ x3 . x3 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (ap x2 x4) x0) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x2 x4) (eps_ x4))) ⟶ (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x2 x5) (ap x2 x4)) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (add_SNo (ap x3 x4) (minus_SNo (eps_ x4))) x0) ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (ap x3 x4)) ⟶ (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x4) (ap x3 x5)) ⟶ SNoCutP {ap x2 x4|x4 ∈ omega} {ap x3 x4|x4 ∈ omega} ⟶ x0 = SNoCut {ap x2 x4|x4 ∈ omega} {ap x3 x4|x4 ∈ omega} ⟶ x1.

Apply real_E with x0, 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: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0.

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

Apply SNo_prereal_incr_lower_approx with x0, x1 leaving 4 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

Let x2 of type ι be given.

Assume H9: (λ x3 . and (x3 ∈ setexp (SNoS_ omega) omega) (∀ x4 . x4 ∈ omega ⟶ and (and (SNoLt (ap x3 x4) x0) (SNoLt x0 (add_SNo (ap x3 x4) (eps_ x4)))) (∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x5) (ap x3 x4)))) x2.

Apply H9 with x1.

Assume H10: x2 ∈ setexp (SNoS_ omega) omega.

Assume H11: ∀ x3 . x3 ∈ omega ⟶ and (and (SNoLt (ap x2 x3) x0) (SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3)))) (∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x4) (ap x2 x3)).

Apply SNo_prereal_decr_upper_approx with x0, x1 leaving 4 subgoals.

The subproof is completed by applying H2.

...

■

Proofgold Proof