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 closed_in X Tx (preimage_of A f ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1))) ∧ closed_in X Tx (preimage_of A f ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1))).
Set I to be the term closed_interval (minus_SNo 1) 1.
Set Ti to be the term closed_interval_topology (minus_SNo 1) 1.
Set I1 to be the term (closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ I.
Set I3 to be the term (closed_interval one_third 1) ∩ I.
We prove the intermediate claim HI1closed: closed_in I Ti I1.
An exact proof term for the current goal is Tietze_I1_closed_in_I.
We prove the intermediate claim HI3closed: closed_in I Ti I3.
An exact proof term for the current goal is Tietze_I3_closed_in_I.
We prove the intermediate claim HBclosedA: closed_in A (subspace_topology X Tx A) (preimage_of A f I1).
An exact proof term for the current goal is (continuous_preserves_closed A (subspace_topology X Tx A) I Ti f Hf I1 HI1closed).
We prove the intermediate claim HCclosedA: closed_in A (subspace_topology X Tx A) (preimage_of A f I3).
An exact proof term for the current goal is (continuous_preserves_closed A (subspace_topology X Tx A) I Ti f Hf I3 HI3closed).
Apply andI to the current goal.
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx A (preimage_of A f I1) HAcl HBclosedA).
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx A (preimage_of A f I3) HAcl HCclosedA).
∎