Let X, Tx and Y be given.
Assume Htop: topology_on X Tx.
Assume HY: Y ⊆ X.
Let U be given.
Assume HU: open_in Y (subspace_topology X Tx Y) U.
We will prove ∃V : set, open_in X Tx V ∧ U = V ∩ Y.
We prove the intermediate claim HtopY: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (andEL (topology_on Y (subspace_topology X Tx Y)) (U ∈ subspace_topology X Tx Y) HU).
We prove the intermediate claim HUinSub: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (U ∈ subspace_topology X Tx Y) HU).
We prove the intermediate claim HUPowerY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (subspace_topology_in_Power X Tx Y U HUinSub).
We prove the intermediate claim HUexists: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HUinSub).
Apply HUexists to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ U = V ∩ Y.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HV).
We prove the intermediate claim HUeqVY: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HV).
We prove the intermediate claim HVopen: open_in X Tx V.
An exact proof term for the current goal is (andI (topology_on X Tx) (V ∈ Tx) Htop HVinTx).
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HUeqVY.
∎