Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H2 with
False leaving 2 subgoals.
Apply In_no2cycle with
u3,
u5 leaving 2 subgoals.
The subproof is completed by applying In_3_5.
The subproof is completed by applying H3.
Assume H3:
and (u5 = u3) (x0 ∈ x1).
Apply H3 with
False.
Apply FalseE with
x0 ∈ x1 ⟶ False.
Apply In_irref with
u3.
Apply H4 with
λ x2 x3 . u3 ∈ x2.
The subproof is completed by applying In_3_5.