Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x0 ∈ x1.
Apply SepI with
V_ x1,
λ x2 . ordinal x2,
9d271.. x0 leaving 2 subgoals.
Apply V_I with
9d271.. x0,
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying Sep_Subq with
V_ x0,
ordinal.
The subproof is completed by applying unknownprop_1ec7349a6007c1951cbc9535ca5769b83316f6778bed19ab211854c4c6028c5d with x0.