Let X, Tx, A and U be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HU: U ∈ Tx.
Assume HAU: A ⊆ U.
We will prove ∃V : set, V ∈ Tx ∧ A ⊆ 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) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ A0 ⊆ U0 ∧ B0 ⊆ V0 ∧ U0 ∩ V0 = Empty) Hnorm).
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 → (normal_space X Tx ↔ ∀A0 U0 : set, closed_in X Tx A0 → U0 ∈ Tx → A0 ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A0 ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0).
An exact proof term for the current goal is (andER (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 ↔ ∀A0 U0 : set, closed_in X Tx A0 → U0 ∈ Tx → A0 ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A0 ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0)) (regular_normal_via_closure X Tx HTx)).
We prove the intermediate claim Hiff: normal_space X Tx ↔ ∀A0 U0 : set, closed_in X Tx A0 → U0 ∈ Tx → A0 ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A0 ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (Hlemma HT1).
We prove the intermediate claim Hcrit: ∀A0 U0 : set, closed_in X Tx A0 → U0 ∈ Tx → A0 ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A0 ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (iffEL (normal_space X Tx) (∀A0 U0 : set, closed_in X Tx A0 → U0 ∈ Tx → A0 ⊆ U0 → ∃V0 : set, V0 ∈ Tx ∧ A0 ⊆ V0 ∧ closure_of X Tx V0 ⊆ U0) Hiff Hnorm).
An exact proof term for the current goal is (Hcrit A U HAcl HU HAU).
∎