Let X and Tx be given.
Assume Harc.
Apply Harc to the current goal.
Let f be given.
Assume Hhom.
We prove the intermediate claim Hcont: continuous_map unit_interval unit_interval_topology X Tx f.
An exact proof term for the current goal is (andEL (continuous_map unit_interval unit_interval_topology X Tx f) (∃g : set, continuous_map X Tx unit_interval unit_interval_topology g ∧ (∀x : set, x ∈ unit_interval → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ X → apply_fun f (apply_fun g y) = y)) Hhom).
We prove the intermediate claim Habc: (topology_on unit_interval unit_interval_topology ∧ topology_on X Tx) ∧ function_on f unit_interval X.
An exact proof term for the current goal is (andEL ((topology_on unit_interval unit_interval_topology ∧ topology_on X Tx) ∧ function_on f unit_interval X) (∀V : set, V ∈ Tx → preimage_of unit_interval f V ∈ unit_interval_topology) Hcont).
We prove the intermediate claim Hab: topology_on unit_interval unit_interval_topology ∧ topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on unit_interval unit_interval_topology ∧ topology_on X Tx) (function_on f unit_interval X) Habc).
An exact proof term for the current goal is (andER (topology_on unit_interval unit_interval_topology) (topology_on X Tx) Hab).
∎