Let x0 of type ι be given.
Assume H2: x0 = 2 ⟶ ∀ x1 : ο . x1.
Assume H3:
∀ x1 . x1 ∈ omega ⟶ x0 = eps_ x1 ⟶ ∀ x2 : ο . x2.
Apply real_E with
x0,
∃ x1 . and (x1 ∈ SNoL_pos x0) (SNoLt x0 (mul_SNo 2 x1)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply dneg with
∃ x1 . and (x1 ∈ omega) (SNoLt (eps_ x1) x0),
∃ x1 . and (x1 ∈ SNoL_pos x0) (SNoLt x0 (mul_SNo 2 x1)) leaving 2 subgoals.
Apply SNoLt_irref with
x0.
Apply H9 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 H4.
Apply abs_SNo_minus with
x0,
λ x2 x3 . SNoLt x3 (eps_ x1) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply pos_abs_SNo with
x0,
λ x2 x3 . SNoLt x3 (eps_ x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply SNoLt_trichotomy_or_impred with
x0,
eps_ x1,
SNoLt x0 (eps_ x1) leaving 5 subgoals.
The subproof is completed by applying H4.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
Assume H13:
x0 = eps_ x1.
Apply FalseE with
SNoLt x0 (eps_ x1).
Apply H3 with
x1 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
Apply FalseE with
SNoLt x0 (eps_ x1).
Apply H11.
Let x2 of type ο be given.
Apply H14 with
x1.
Apply andI with
x1 ∈ omega,
SNoLt (eps_ x1) x0 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H1.
Let x1 of type ι be given.