Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply iffI with
x2 ∈ ap x0 x1,
setsum x1 x2 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying apE with x0, x1, x2.
The subproof is completed by applying apI with x0, x1, x2.