Let X, U and V be given.

Assume HU: U ∈ 𝒫 X.

Assume HV: V ∈ 𝒫 X.

We will prove U ∩ V ∈ 𝒫 X.

Apply PowerI to the current goal.

Let x be given.

Assume Hx: x ∈ U ∩ V.

We will prove x ∈ X.

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (binintersectE1 U V x Hx).

We prove the intermediate claim HUsub: U ⊆ X.

An exact proof term for the current goal is (PowerE X U HU).

An exact proof term for the current goal is (HUsub x HxU).

∎