Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H1: x1 ∈ x0.
Apply ordinal_ordsucc_In_Subq with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply ordinal_In_Or_Subq with
ordsucc x1,
x0,
ordsucc x1 ∈ ordsucc x0 leaving 4 subgoals.
Apply ordinal_ordsucc with
x1.
Apply ordinal_Hered with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply ordsuccI1 with
x0,
ordsucc x1.
The subproof is completed by applying H3.
Apply set_ext with
ordsucc x1,
x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
Apply L4 with
λ x2 x3 . x3 ∈ ordsucc x0.
The subproof is completed by applying ordsuccI2 with x0.