Let A, U and V be given.

Assume HUV.

Let x be given.

Assume Hx.

Apply setminusE A V x Hx to the current goal.

Assume H1 H2.

Apply setminusI to the current goal.

An exact proof term for the current goal is H1.

Assume H3: x ∈ U.

Apply H2 to the current goal.

We will prove x ∈ V.

An exact proof term for the current goal is HUV x H3.

∎