Let X, Tx and x be given.
Assume Hconn: connected_space X Tx.
Assume HxX: x ∈ X.
We will prove component_of X Tx x = X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (connected_space_topology X Tx Hconn).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ component_of X Tx x.
We will prove y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
Let y be given.
Assume HyX: y ∈ X.
We will prove y ∈ component_of X Tx x.
We will prove y ∈ {y0 ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
We prove the intermediate claim Hsubeq: subspace_topology X Tx X = Tx.
An exact proof term for the current goal is (subspace_topology_whole X Tx HTx).
We prove the intermediate claim HconnSub: connected_space X (subspace_topology X Tx X).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is Hconn.
We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
We use X to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HconnSub.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HyX.
∎