Let X, Tx and U be given.
Assume H: partition_of_unity_dominated X Tx U.
We prove the intermediate claim Hpair: topology_on X Tx ∧ open_cover X Tx U.
An exact proof term for the current goal is (partition_of_unity_dominated_topology_open_cover X Tx U H).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (open_cover X Tx U) Hpair).
We prove the intermediate claim HUcov: open_cover X Tx U.
An exact proof term for the current goal is (andER (topology_on X Tx) (open_cover X Tx U) Hpair).
An exact proof term for the current goal is (open_cover_family_sub X Tx U HTx HUcov).
∎