Let X and Tx be given.

Assume HTx: topology_on X Tx.

Let x be given.

Assume Hx: x ∈ X.

We will prove closed_in X Tx (component_of X Tx x).

Set A to be the term component_of X Tx x.

Set B to be the term closure_of X Tx A.

We prove the intermediate claim HBdef: B = closure_of X Tx A.

Use reflexivity.

We prove the intermediate claim HAsub: A ⊆ X.

Let y be given.

Assume Hy: y ∈ A.

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).

We prove the intermediate claim HBsub: B ⊆ X.

rewrite the current goal using HBdef (from left to right).

An exact proof term for the current goal is (closure_in_space X Tx A HTx).

We prove the intermediate claim HAB: A ⊆ B.

rewrite the current goal using HBdef (from left to right).

An exact proof term for the current goal is (subset_of_closure X Tx A HTx HAsub).

We prove the intermediate claim HAconn: connected_space A (subspace_topology X Tx A).

An exact proof term for the current goal is (component_of_connected X Tx x HTx Hx).

We prove the intermediate claim HBcl: B ⊆ closure_of X Tx A.

rewrite the current goal using HBdef (from left to right).

An exact proof term for the current goal is (Subq_ref (closure_of X Tx A)).

We prove the intermediate claim HBconn: connected_space B (subspace_topology X Tx B).

An exact proof term for the current goal is (connected_with_limit_points X Tx A B HTx HAsub HBsub HAconn HAB HBcl).

We prove the intermediate claim HBsubA: B ⊆ A.

Let y be given.

Assume Hy: y ∈ B.

We will prove y ∈ A.

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 (HBsub y Hy).

We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.

We use B to witness the existential quantifier.

We will prove connected_space B (subspace_topology X Tx B) ∧ x ∈ B ∧ y ∈ B.

Apply andI to the current goal.

An exact proof term for the current goal is HBconn.

We prove the intermediate claim HxA: x ∈ A.

An exact proof term for the current goal is (point_in_component X Tx x HTx Hx).

An exact proof term for the current goal is (HAB x HxA).

An exact proof term for the current goal is Hy.

We prove the intermediate claim Heq: B = A.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ B.

An exact proof term for the current goal is (HBsubA y Hy).

Let y be given.

Assume Hy: y ∈ A.

An exact proof term for the current goal is (HAB y Hy).

We prove the intermediate claim HBclosed0: closed_in X Tx (closure_of X Tx A).

An exact proof term for the current goal is (closure_is_closed X Tx A HTx HAsub).

We prove the intermediate claim HBclosed: closed_in X Tx B.

rewrite the current goal using HBdef (from right to left).

An exact proof term for the current goal is HBclosed0.

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

rewrite the current goal using Heq (from right to left).

An exact proof term for the current goal is HBclosed.

An exact proof term for the current goal is HAclosed.

∎