Let X, Tx, Y, U and V be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
Assume HU: U ∈ subspace_topology X Tx Y.
Assume HV: V ∈ subspace_topology X Tx Y.
We prove the intermediate claim HexU: ∃VU ∈ Tx, U = VU ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).
We prove the intermediate claim HexV: ∃VV ∈ Tx, V = VV ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y V HV).
Apply HexU to the current goal.
Let VU be given.
Assume HVUpair.
We prove the intermediate claim HVU: VU ∈ Tx.
An exact proof term for the current goal is (andEL (VU ∈ Tx) (U = VU ∩ Y) HVUpair).
We prove the intermediate claim HUeq: U = VU ∩ Y.
An exact proof term for the current goal is (andER (VU ∈ Tx) (U = VU ∩ Y) HVUpair).
Apply HexV to the current goal.
Let VV be given.
Assume HVVpair.
We prove the intermediate claim HVV: VV ∈ Tx.
An exact proof term for the current goal is (andEL (VV ∈ Tx) (V = VV ∩ Y) HVVpair).
We prove the intermediate claim HVeq: V = VV ∩ Y.
An exact proof term for the current goal is (andER (VV ∈ Tx) (V = VV ∩ Y) HVVpair).
We prove the intermediate claim HUV: VU ∩ VV ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx VU VV HTx HVU HVV).
rewrite the current goal using (subspace_topology_binintersect_witness X Tx Y U V VU VV HUeq HVeq) (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y (VU ∩ VV) HUV).
∎