Let x0 of type ι be given.

Assume H0: SNo x0.

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

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

Apply SNo_prereal_incr_lower_approx with minus_SNo x0, ∃ x1 . and (x1 ∈ setexp (SNoS_ omega) omega) (∀ x2 . x2 ∈ omega ⟶ and (and (SNoLt (add_SNo (ap x1 x2) (minus_SNo (eps_ x2))) x0) (SNoLt x0 (ap x1 x2))) (∀ x3 . x3 ∈ x2 ⟶ SNoLt (ap x1 x2) (ap x1 x3))) leaving 4 subgoals.

Apply SNo_minus_SNo with x0.

The subproof is completed by applying H0.

Apply minus_SNo_prereal_1 with x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply minus_SNo_prereal_2 with x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

Let x1 of type ι be given.

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

Apply H3 with ∃ x2 . and (x2 ∈ setexp (SNoS_ omega) omega) (∀ x3 . x3 ∈ omega ⟶ and (and (SNoLt (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0) (SNoLt x0 (ap x2 x3))) (∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x3) (ap x2 x4))).

Assume H4: x1 ∈ setexp (SNoS_ omega) omega.

Assume H5: ∀ x2 . x2 ∈ omega ⟶ and (and (SNoLt (ap x1 x2) (minus_SNo x0)) (SNoLt (minus_SNo x0) (add_SNo (ap x1 x2) (eps_ x2)))) (∀ x3 . x3 ∈ x2 ⟶ SNoLt (ap x1 x3) (ap x1 x2)).

Claim L6: ...

...

Let x2 of type ο be given.

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

Apply H7 with lam omega (λ x3 . minus_SNo (ap x1 x3)).

Apply andI with lam ... ... ∈ ..., ... leaving 2 subgoals.

...

■

Proofgold Proof