Let X and Tx be given.
Assume Hcr: completely_regular_space X Tx.
We will prove one_point_sets_closed 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.
We prove the intermediate claim Hrest: 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 (andER (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).
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 → ∃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) Hrest).
∎