Let x0 of type ι be given.
Apply dneg with
∃ x1 . and (x1 ∈ real) (mul_SNo x0 x1 = 1).
Apply real_E with
x0,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoCutP_SNoCut_impred with
{x1 ∈ SNoS_ omega|SNoLt (mul_SNo x0 x1) 1},
{x1 ∈ SNoS_ omega|SNoLt 1 (mul_SNo x0 x1)},
False leaving 2 subgoals.
Apply and3I with
∀ x1 . x1 ∈ {x2 ∈ SNoS_ omega|SNoLt (mul_SNo x0 x2) 1} ⟶ SNo x1,
∀ x1 . x1 ∈ {x2 ∈ SNoS_ omega|SNoLt 1 (mul_SNo x0 x2)} ⟶ SNo x1,
∀ x1 . x1 ∈ {x2 ∈ SNoS_ omega|SNoLt (mul_SNo x0 x2) 1} ⟶ ∀ x2 . x2 ∈ {x3 ∈ SNoS_ omega|SNoLt 1 (mul_SNo x0 x3)} ⟶ SNoLt x1 x2 leaving 3 subgoals.
Let x1 of type ι be given.
Apply L11 with
x1,
SNo x1 leaving 2 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x1 of type ι be given.
Apply L12 with
x1,
SNo x1 leaving 2 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply L11 with
x1,
SNoLt x1 x2 leaving 2 subgoals.
The subproof is completed by applying H13.
Apply L12 with
x2,
SNoLt x1 x2 leaving 2 subgoals.
The subproof is completed by applying H14.