Let x0 of type ι be given.
Apply dneg with
∃ x1 . and (x1 ∈ omega) (SNoLt (eps_ x1) x0).
Apply real_E with
x0,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoLt_irref with
x0.
Apply H8 with
0,
λ x1 x2 . SNoLt x1 x0 leaving 3 subgoals.
Apply SNoS_I with
omega,
0,
0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply ordinal_SNo_ with
0.
The subproof is completed by applying ordinal_Empty.
Let x1 of type ι be given.
Apply add_SNo_0L with
minus_SNo x0,
λ x2 x3 . SNoLt (abs_SNo x3) (eps_ x1) leaving 2 subgoals.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H3.
Apply abs_SNo_minus with
x0,
λ x2 x3 . SNoLt x3 (eps_ x1) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply nonneg_abs_SNo with
x0,
λ x2 x3 . SNoLt x3 (eps_ x1) leaving 2 subgoals.
Apply SNoLtLe with
0,
x0.
The subproof is completed by applying H1.
Apply SNoLtLe_or with
x0,
eps_ x1,
SNoLt x0 (eps_ x1) leaving 4 subgoals.
The subproof is completed by applying H3.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Apply FalseE with
SNoLt x0 (eps_ x1).
Apply H2.
Let x2 of type ο be given.
Apply H12 with
ordsucc x1.
Apply andI with
ordsucc x1 ∈ omega,
SNoLt (eps_ (ordsucc x1)) x0 leaving 2 subgoals.
Apply omega_ordsucc with
x1.
The subproof is completed by applying H10.
Apply SNoLtLe_tra with
eps_ (ordsucc x1),
eps_ x1,
x0 leaving 5 subgoals.
Apply SNo_eps_ with
ordsucc x1.
Apply omega_ordsucc with
x1.
The subproof is completed by applying H10.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H10.
The subproof is completed by applying H3.
Apply eps_ordsucc_Lt with
x1.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H1.