Let X, Tx and U be given.

Assume HTx: topology_on X Tx.

Assume Hcov: open_cover X Tx U.

Assume HUfin: finite U.

We will prove locally_finite_family X Tx U.

We prove the intermediate claim HUsubPow: U ⊆ 𝒫 X.

An exact proof term for the current goal is (open_cover_family_sub X Tx U HTx Hcov).

An exact proof term for the current goal is (finite_family_locally_finite X Tx U HTx HUfin HUsubPow).

∎