Let x0 of type ι be given.
Apply set_ext with
proj0 x0,
ap x0 0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0:
x1 ∈ proj0 x0.
Apply apI with
x0,
0,
x1.
Apply proj0E with
x0,
x1.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply proj0I with
x0,
x1.
Apply apE with
x0,
0,
x1.
The subproof is completed by applying H0.