Let x0 of type ι be given.
Apply set_ext with
proj1 x0,
ap x0 1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0:
x1 ∈ proj1 x0.
Apply apI with
x0,
1,
x1.
Apply proj1E with
x0,
x1.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply proj1I with
x0,
x1.
Apply apE with
x0,
1,
x1.
The subproof is completed by applying H0.