Let X, Tx, x and U be given.

Assume HxX: x ∈ X.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We will prove ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U.

We prove the intermediate claim HT1: one_point_sets_closed X Tx.

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F : set, closed_in X Tx F → x0 ∉ F → ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x0 ∈ U0 ∧ F ⊆ V0 ∧ U0 ∩ V0 = Empty) Hreg).

We prove the intermediate claim HTx: topology_on X Tx.

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

We prove the intermediate claim Hlemma: one_point_sets_closed X Tx → (regular_space X Tx ↔ ∀x0 U0 : set, x0 ∈ X → U0 ∈ Tx → x0 ∈ U0 → ∃V0 : set, V0 ∈ Tx ∧ x0 ∈ V0 ∧ closure_of X Tx V0 ⊆ U0).

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx → (regular_space X Tx ↔ ∀x0 U0 : set, x0 ∈ X → U0 ∈ Tx → x0 ∈ U0 → ∃V0 : set, V0 ∈ Tx ∧ x0 ∈ V0 ∧ closure_of X Tx V0 ⊆ U0)) (one_point_sets_closed X Tx → (normal_space X Tx ↔ ∀A U0 : set, closed_in X Tx A → U0 ∈ Tx → A ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0)) (regular_normal_via_closure X Tx HTx)).

We prove the intermediate claim Hiff: regular_space X Tx ↔ ∀x0 U0 : set, x0 ∈ X → U0 ∈ Tx → x0 ∈ U0 → ∃V0 : set, V0 ∈ Tx ∧ x0 ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (Hlemma HT1).

We prove the intermediate claim Hcrit: ∀x0 U0 : set, x0 ∈ X → U0 ∈ Tx → x0 ∈ U0 → ∃V0 : set, V0 ∈ Tx ∧ x0 ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.

An exact proof term for the current goal is (iffEL (regular_space X Tx) (∀x0 U0 : set, x0 ∈ X → U0 ∈ Tx → x0 ∈ U0 → ∃V0 : set, V0 ∈ Tx ∧ x0 ∈ V0 ∧ closure_of X Tx V0 ⊆ U0) Hiff Hreg).

An exact proof term for the current goal is (Hcrit x U HxX HU HxU).

∎