Let X, x and Y be given.

Assume H1: x ∈ Y.

Assume H2: Y ∈ X.

Apply UnionEq X x to the current goal.

Assume _ H3.

Apply H3 to the current goal.

We will prove ∃Y : set, x ∈ Y ∧ Y ∈ X.

We use Y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

∎