Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ReplE_impred with
x1,
λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2,
x0,
False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x1.
Apply tagged_not_ordinal with
x2.
Apply H3 with
λ x3 x4 . ordinal x3.
The subproof is completed by applying H0.