Let X, Y and z be given.

Assume H1: z ∈ Y.

We will prove z ∈ X ∪ Y.

We will prove z ∈ ⋃ {X,Y}.

Apply (UnionI {X,Y} z Y) to the current goal.

We will prove z ∈ Y.

An exact proof term for the current goal is H1.

We will prove Y ∈ {X,Y}.

An exact proof term for the current goal is (UPairI2 X Y).

∎