Let X, Tx and A be given.
Assume HTx: topology_on X Tx.
Assume HAsub: A ⊆ X.
Assume HAconn: connected_space A (subspace_topology X Tx A).
Assume Hdense: closure_of X Tx A = X.
We will prove connected_space X Tx.
We will prove topology_on X Tx ∧ ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We will prove ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).
Assume Hsep: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.
Apply HexV to the current goal.
Let V be given.
Assume HUVsep.
We prove the intermediate claim HUV12: U ∈ Tx ∧ V ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUVsep).
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) HUV12).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) HUV12).
We prove the intermediate claim HsepUV: separation_of X U V.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUVsep).
We prove the intermediate claim HsepL: ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) HsepUV).
We prove the intermediate claim HUVdisj: (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) HsepL)).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) HUVdisj).
We prove the intermediate claim HU0: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) HsepL)).
We prove the intermediate claim HV0: V ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) HsepL).
We prove the intermediate claim Hside: A ⊆ U ∨ A ⊆ V.
An exact proof term for the current goal is (connected_subset_in_separation_side X Tx U V A HTx HAsub HAconn HU HV HsepUV).
Apply Hside to the current goal.
Assume HAU: A ⊆ U.
We prove the intermediate claim HVneA: V ∩ A ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open A X Tx V HTx Hdense HV HV0).
We prove the intermediate claim HVAsubEmpty: V ∩ A ⊆ Empty.
Let x be given.
Assume Hx: x ∈ V ∩ A.
We will prove x ∈ Empty.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 V A x Hx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HAU x HxA).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVempty (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is HxE.
We prove the intermediate claim HVAEq: V ∩ A = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (V ∩ A) HVAsubEmpty).
Apply HVneA to the current goal.
An exact proof term for the current goal is HVAEq.
Assume HAV: A ⊆ V.
We prove the intermediate claim HUneA: U ∩ A ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open A X Tx U HTx Hdense HU HU0).
We prove the intermediate claim HUAsubEmpty: U ∩ A ⊆ Empty.
Let x be given.
Assume Hx: x ∈ U ∩ A.
We will prove x ∈ Empty.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 U A x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HAV x HxA).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVempty (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is HxE.
We prove the intermediate claim HUAEq: U ∩ A = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U ∩ A) HUAsubEmpty).
Apply HUneA to the current goal.
An exact proof term for the current goal is HUAEq.
∎