Assume HT1: T1_space X Tx.

We will prove ∀x : set, x ∈ X → closed_in X Tx {x}.

Let x be given.

Assume Hx: x ∈ X.

We will prove closed_in X Tx {x}.

We prove the intermediate claim Hx_finite: finite {x}.

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

We prove the intermediate claim Hx_sub: {x} ⊆ X.

Let y be given.

Assume Hy: y ∈ {x}.

We prove the intermediate claim Hyeq: y = x.

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

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

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is (T1_space_finite_closed X Tx {x} HT1 Hx_sub Hx_finite).

Assume Hsing: ∀x : set, x ∈ X → closed_in X Tx {x}.

We will prove T1_space X Tx.

We will prove topology_on X Tx ∧ (∀F : set, F ⊆ X → finite F → closed_in X Tx F).

Apply andI to the current goal.

An exact proof term for the current goal is Htop.

We will prove ∀F : set, F ⊆ X → finite F → closed_in X Tx F.

Let F be given.

Assume HFsub: F ⊆ X.

Assume HF: finite F.

We will prove closed_in X Tx F.

We prove the intermediate claim Hclosed_empty: closed_in X Tx Empty.

An exact proof term for the current goal is (empty_is_closed X Tx Htop).

We prove the intermediate claim Hclosed_union: ∀A B : set, closed_in X Tx A → closed_in X Tx B → closed_in X Tx (A ∪ B).

Let A and B be given.

Assume HA.

Assume HB.

An exact proof term for the current goal is (union_of_closed_is_closed X Tx A B Htop HA HB).

We prove the intermediate claim Hall: ∀F0 : set, finite F0 → (F0 ⊆ X → closed_in X Tx F0).

An exact proof term for the current goal is (finite_ind (λF0 : set ⇒ F0 ⊆ X → closed_in X Tx F0) (λ_ ⇒ Hclosed_empty) (λF0 y : set ⇒ λHFin0 HyNotin IH ⇒ λHsubUnion ⇒ Hclosed_union F0 {y} (IH (λz Hz ⇒ HsubUnion z (binunionI1 F0 {y} z Hz))) (Hsing y (HsubUnion y (binunionI2 F0 {y} y (SingI y)))))).

We prove the intermediate claim Hspec: F ⊆ X → closed_in X Tx F.

An exact proof term for the current goal is (Hall F HF).

An exact proof term for the current goal is (Hspec HFsub).