Let X and Tx be given.

Assume Hnorm: normal_space X Tx.

We will prove topology_on X Tx.

We prove the intermediate claim Hone: one_point_sets_closed X Tx.

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).

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

∎