Let X and U be given.

Assume HU: U ∈ 𝒫 X.

We will prove X ∖ U ∈ 𝒫 X.

Apply PowerI to the current goal.

Let x be given.

Assume Hx: x ∈ X ∖ U.

We will prove x ∈ X.

An exact proof term for the current goal is (setminusE1 X U x Hx).

∎