Let X, T and U be given.
Assume HU: open_in X T U.
We will prove U ⊆ X.
We prove the intermediate claim HTx: topology_on X T.
An exact proof term for the current goal is (open_in_topology X T U HU).
We prove the intermediate claim HUT: U ∈ T.
An exact proof term for the current goal is (open_in_elem X T U HU).
We prove the intermediate claim HUPower: U ∈ 𝒫 X.
An exact proof term for the current goal is ((topology_sub_Power X T HTx) U HUT).
An exact proof term for the current goal is (PowerE X U HUPower).
∎