Let X, Tx, Fam and Sub be given.

Assume HLF: locally_finite_family X Tx Fam.

Assume HSub: Sub ⊆ Fam.

An exact proof term for the current goal is (locally_finite_subfamily X Tx Fam Sub HLF HSub).

∎