Let X, Tx, Y and U be given.

Assume HTx: topology_on X Tx.

Assume HY: Y ∈ Tx.

Assume HU: U ⊆ Y.

Assume HUopen: open_in Y (subspace_topology X Tx Y) U.

We will prove U ∈ Tx.

We prove the intermediate claim HYsub: Y ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx Y HTx HY).

We prove the intermediate claim HUiffExists: open_in Y (subspace_topology X Tx Y) U ↔ ∃V ∈ Tx, U = V ∩ Y.

An exact proof term for the current goal is (open_in_subspace_iff X Tx Y U HTx HYsub HU).

We prove the intermediate claim Hexists: ∃V ∈ Tx, U = V ∩ Y.

An exact proof term for the current goal is (iffEL (open_in Y (subspace_topology X Tx Y) U) (∃V ∈ Tx, U = V ∩ Y) HUiffExists HUopen).

Apply Hexists to the current goal.

Let V be given.

Assume HVandEq.

Apply HVandEq to the current goal.

Assume HV: V ∈ Tx.

Assume HUeq: U = V ∩ Y.

We prove the intermediate claim HVY: V ∩ Y ∈ Tx.

An exact proof term for the current goal is (topology_binintersect_closed X Tx V Y HTx HV HY).

We prove the intermediate claim HUinTx: U ∈ Tx.

rewrite the current goal using HUeq (from left to right).

An exact proof term for the current goal is HVY.

An exact proof term for the current goal is HUinTx.

∎