Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ real.

Apply real_E with x0, ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: SNo x0.

Assume H2: SNoLev x0 ∈ ordsucc omega.

Assume H3: x0 ∈ SNoS_ (ordsucc omega).

Assume H4: SNoLt (minus_SNo omega) x0.

Assume H5: SNoLt x0 omega.

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

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

The subproof is completed by applying H6.

■