Let X, Tx, Y and U be given.

Assume HU: U ∈ subspace_topology X Tx 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).

Apply Hex to the current goal.

Let V be given.

Assume HVpair.

We prove the intermediate claim HUeq: U = V ∩ Y.

An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVpair).

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

An exact proof term for the current goal is (binintersect_Subq_2 V Y).

∎