We will prove ¬ (∃A : set, A ≠ Empty ∧ A ≠ X ∧ open_in X Tx A ∧ closed_in X Tx A).

Assume Hclopen: ∃A : set, A ≠ Empty ∧ A ≠ X ∧ open_in X Tx A ∧ closed_in X Tx A.

We prove the intermediate claim Hnosep: ¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V).

An exact proof term for the current goal is (andER (topology_on X Tx) (¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V)) Hconn).

Apply Hclopen to the current goal.

Let A be given.

Assume HA.

We prove the intermediate claim HAne: A ≠ Empty.

An exact proof term for the current goal is (andEL (A ≠ Empty) (A ≠ X) (andEL (A ≠ Empty ∧ A ≠ X) (open_in X Tx A) (andEL ((A ≠ Empty ∧ A ≠ X) ∧ open_in X Tx A) (closed_in X Tx A) HA))).

We prove the intermediate claim HAnX: A ≠ X.

An exact proof term for the current goal is (andER (A ≠ Empty) (A ≠ X) (andEL (A ≠ Empty ∧ A ≠ X) (open_in X Tx A) (andEL ((A ≠ Empty ∧ A ≠ X) ∧ open_in X Tx A) (closed_in X Tx A) HA))).

We prove the intermediate claim HAopen: open_in X Tx A.

An exact proof term for the current goal is (andER (A ≠ Empty ∧ A ≠ X) (open_in X Tx A) (andEL ((A ≠ Empty ∧ A ≠ X) ∧ open_in X Tx A) (closed_in X Tx A) HA)).

We prove the intermediate claim HAclosed: closed_in X Tx A.

An exact proof term for the current goal is (andER ((A ≠ Empty ∧ A ≠ X) ∧ open_in X Tx A) (closed_in X Tx A) HA).

We prove the intermediate claim Hsepexists: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.

An exact proof term for the current goal is (clopen_gives_separation X Tx A HTx HAne HAnX HAopen HAclosed).

Apply Hnosep to the current goal.

An exact proof term for the current goal is Hsepexists.

Assume Hno_clopen: ¬ (∃A : set, A ≠ Empty ∧ A ≠ X ∧ open_in X Tx A ∧ closed_in X Tx A).

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 HsepV: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V.

Apply HsepV to the current goal.

Let V be given.

Assume HUV.

We prove the intermediate claim HU: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV)).

We prove the intermediate claim HV: V ∈ Tx.

An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV)).

We prove the intermediate claim Hsepof: separation_of X U V.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (separation_of X U V) HUV).

We prove the intermediate claim Hclopenexists: ∃A : set, A ≠ Empty ∧ A ≠ X ∧ open_in X Tx A ∧ closed_in X Tx A.

An exact proof term for the current goal is (separation_gives_clopen X Tx U V HTx HU HV Hsepof).

Apply Hno_clopen to the current goal.

An exact proof term for the current goal is Hclopenexists.