Let X, Tx, A and f be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume Hf: continuous_map A (subspace_topology X Tx A) (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) f.
We will prove ∃g : set, continuous_map X Tx (closed_interval (minus_SNo one_third) one_third) (closed_interval_topology (minus_SNo one_third) one_third) g ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g x = minus_SNo one_third) ∧ (∀x : set, x ∈ preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)) → apply_fun g x = one_third).
Set B to be the term preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)).
Set C to be the term preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)).
We prove the intermediate claim HBCclosed: closed_in X Tx B ∧ closed_in X Tx C.
An exact proof term for the current goal is (Tietze_stepI_BC_closed_in_X X Tx A f Hnorm HAcl Hf).
We prove the intermediate claim HBcl: closed_in X Tx B.
An exact proof term for the current goal is (andEL (closed_in X Tx B) (closed_in X Tx C) HBCclosed).
We prove the intermediate claim HCcl: closed_in X Tx C.
An exact proof term for the current goal is (andER (closed_in X Tx B) (closed_in X Tx C) HBCclosed).
We prove the intermediate claim Hdisj: B ∩ C = Empty.
rewrite the current goal using (preimage_of_binintersect A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)) ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1))) (from right to left).
rewrite the current goal using Tietze_I1_I3_disjoint (from left to right).
An exact proof term for the current goal is (preimage_of_Empty A f).
We prove the intermediate claim Hm13le13: Rle (minus_SNo one_third) one_third.
An exact proof term for the current goal is Rle_minus_one_third_one_third.
An exact proof term for the current goal is (Urysohn_lemma X Tx B C (minus_SNo one_third) one_third Hm13le13 Hnorm HBcl HCcl Hdisj).
∎