Let X, Tx and U be given.

Assume HTx: topology_on X Tx.

Assume _: open_cover X Tx U.

Assume HUfin: finite U.

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

∎