Let X, Y and Z be given.

Assume H1: X ⊆ Z.

Assume H2: Y ⊆ Z.

Let w be given.

Assume H3: w ∈ X ∪ Y.

Apply (binunionE X Y w H3) to the current goal.

Assume H4: w ∈ X.

An exact proof term for the current goal is (H1 w H4).

Assume H4: w ∈ Y.

An exact proof term for the current goal is (H2 w H4).

∎