Let X, T and U be given.

Assume HTx: topology_on X T.

Assume HU: U ∈ T.

We will prove U ⊆ X.

We prove the intermediate claim HUPower: U ∈ 𝒫 X.

An exact proof term for the current goal is ((topology_sub_Power X T HTx) U HU).

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

∎