Let x0 of type ι be given.
Apply nat_ind with
λ x1 . atleastp x1 x0 ⟶ x1 ⊆ x0 leaving 2 subgoals.
The subproof is completed by applying Subq_Empty with x0.
Let x1 of type ι be given.
Apply atleastp_tra with
x1,
ordsucc x1,
x0 leaving 2 subgoals.
Apply Subq_atleastp with
x1,
ordsucc x1.
The subproof is completed by applying ordsuccI1 with x1.
The subproof is completed by applying H3.
Claim L5: x1 ⊆ x0
Apply H2.
The subproof is completed by applying L4.
Apply ordinal_In_Or_Subq with
x0,
ordsucc x1,
ordsucc x1 ⊆ x0 leaving 4 subgoals.
Apply nat_p_ordinal with
x0.
The subproof is completed by applying H0.
Apply nat_p_ordinal with
ordsucc x1.
Apply nat_ordsucc with
x1.
The subproof is completed by applying H1.
Apply FalseE with
ordsucc x1 ⊆ x0.
Apply ordsuccE with
x1,
x0,
False leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H7: x0 ∈ x1.
Apply In_irref with
x0.
Apply L5 with
x0.
The subproof is completed by applying H7.
Assume H7: x0 = x1.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H7 with
λ x2 x3 . atleastp (ordsucc x1) x2.
The subproof is completed by applying H3.
The subproof is completed by applying H6.