Let X and Tx be given.
Assume Hreg: regular_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) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) Hone).
∎