Let x0 of type ι be given.
Apply H0 with
False.
Apply H2 with
(∀ x1 . x1 ∈ omega ⟶ divides_nat x1 x0 ⟶ or (x1 = 1) (x1 = x0)) ⟶ False.
Assume H4: 1 ∈ x0.
Apply SNoLt_irref with
1.
Apply SNoLtLe_tra with
1,
x0,
1 leaving 5 subgoals.
The subproof is completed by applying SNo_1.
Apply nat_p_SNo with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
The subproof is completed by applying SNo_1.
Apply ordinal_In_SNoLt with
x0,
1 leaving 2 subgoals.
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply divides_int_pos_Le with
x0,
1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying SNoLt_0_1.