Let X and Tx be given.

Assume Hcr: completely_regular_space X Tx.

We will prove topology_on X Tx.

We prove the intermediate claim Hdef: topology_on X Tx ∧ (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1).

An exact proof term for the current goal is Hcr.

An exact proof term for the current goal is (andEL (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1) Hdef).

∎