Let X, Tx and C be given.
Assume HTx: topology_on X Tx.
Assume HCconn: connected_space C (subspace_topology X Tx C).
We will prove C ⊆ X.
We prove the intermediate claim HCtop: topology_on C (subspace_topology X Tx C).
An exact proof term for the current goal is (connected_space_topology C (subspace_topology X Tx C) HCconn).
We prove the intermediate claim HCinSub: C ∈ subspace_topology X Tx C.
An exact proof term for the current goal is (topology_has_X C (subspace_topology X Tx C) HCtop).
We prove the intermediate claim HexV: ∃V ∈ Tx, C = V ∩ C.
An exact proof term for the current goal is (subspace_topologyE X Tx C C HCinSub).
Apply HexV to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (C = V ∩ C) HVpair).
We prove the intermediate claim HCeq: C = V ∩ C.
An exact proof term for the current goal is (andER (V ∈ Tx) (C = V ∩ C) HVpair).
We prove the intermediate claim HCsubV: C ⊆ V.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (binintersect_Subq_1 V C).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVTx).
An exact proof term for the current goal is (Subq_tra C V X HCsubV HVsubX).
∎