Let X, Tx and x be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
We will prove x ∈ component_of X Tx x.
We will prove x ∈ {y ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ x ∈ C.
We use {x} to witness the existential quantifier.
We will prove connected_space {x} (subspace_topology X Tx {x}) ∧ x ∈ {x} ∧ x ∈ {x}.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (singleton_subspace_connected X Tx x HTx HxX).
An exact proof term for the current goal is (SingI x).
An exact proof term for the current goal is (SingI x).
∎