Let X, Tx and Fam be given.

Assume Hof: open_cover_of X Tx Fam.

Assume HFamFin: finite Fam.

We will prove locally_finite_family X Tx Fam.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (open_cover_of_topology X Tx Fam Hof).

We prove the intermediate claim HFamSubPow: Fam ⊆ 𝒫 X.

An exact proof term for the current goal is (open_cover_of_family_sub X Tx Fam Hof).

An exact proof term for the current goal is (finite_family_locally_finite X Tx Fam HTx HFamFin HFamSubPow).

∎