Let X and Tx be given.

Assume HXconn: connected_space X Tx.

Assume HXreg: regular_space X Tx.

Assume Hex: ∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y.

We will prove ¬ countable X.

Assume HcountX: countable X.

We prove the intermediate claim Hone: one_point_sets_closed X Tx.

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) HXreg).

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) Hone).

We prove the intermediate claim HL: Lindelof_space X Tx.

An exact proof term for the current goal is (countable_space_implies_Lindelof_space X Tx HTx HcountX).

We prove the intermediate claim HN: normal_space X Tx.

An exact proof term for the current goal is (ex32_4_regular_Lindelof_normal X Tx HXreg HL).

An exact proof term for the current goal is (ex33_2a_connected_normal_uncountable X Tx HXconn HN Hex HcountX).

∎