Apply unknownprop_247eca63ddbcabcce23f37444296e0737b3d081ddee4a41779d4f9a2c3d52966 with
{x0 ∈ real|natOfOrderedField_p real 0 1 add_SNo mul_SNo SNoLe x0},
0,
λ x0 . add_SNo x0 1,
{x0 ∈ real|natOfOrderedField_p real 0 1 add_SNo mul_SNo SNoLe x0} = omega leaving 2 subgoals.
Apply explicit_Nats_natOfOrderedField with
real,
0,
1,
add_SNo,
mul_SNo,
SNoLe.
The subproof is completed by applying explicit_OrderedField_real.
Apply set_ext with
{x0 ∈ real|natOfOrderedField_p real 0 1 add_SNo mul_SNo SNoLe x0},
omega leaving 2 subgoals.
Apply H4 with
λ x0 . x0 ∈ omega leaving 2 subgoals.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Let x0 of type ι be given.
Apply add_SNo_1_ordsucc with
x0,
λ x1 x2 . x2 ∈ omega leaving 2 subgoals.
The subproof is completed by applying H5.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H5.
Let x0 of type ι be given.
Apply nat_ind with
λ x1 . x1 ∈ {x2 ∈ real|natOfOrderedField_p real 0 1 add_SNo mul_SNo SNoLe x2},
x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply add_SNo_1_ordsucc with
x1,
λ x2 x3 . x2 ∈ {x4 ∈ real|natOfOrderedField_p real 0 1 add_SNo mul_SNo SNoLe x4} leaving 2 subgoals.
Apply nat_p_omega with
x1.
The subproof is completed by applying H6.
Apply H1 with
x1.
The subproof is completed by applying H7.
Apply omega_nat_p with
x0.
The subproof is completed by applying H5.