Let X, Tx, Y and U be given.
Assume HU: U ∈ subspace_topology X Tx Y.
We will prove (ambient_open_of_subspace_open X Tx Y U) ∈ Tx ∧ U = (ambient_open_of_subspace_open X Tx Y U) ∩ Y.
We prove the intermediate claim Hex: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Tx ∧ U = V ∩ Y) Hex).
∎