Let X, Tx, x and F be given.
Assume Hcr: completely_regular_space X Tx.
Assume HxX: x ∈ X.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃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.
We prove the intermediate claim Hdef: topology_on X Tx ∧ (one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1).
An exact proof term for the current goal is Hcr.
We prove the intermediate claim Hrest: one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1.
An exact proof term for the current goal is (andER (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1) Hdef).
We prove the intermediate claim Hforall: ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f0 : set, continuous_map X Tx R R_standard_topology f0 ∧ apply_fun f0 x0 = 0 ∧ ∀y0 : set, y0 ∈ F0 → apply_fun f0 y0 = 1) Hrest).
An exact proof term for the current goal is (Hforall x HxX F HFcl HxnotF).
∎