Let X, Tx and Fam be given.

Assume _: ∀A : set, A ∈ Fam → A ⊆ X.

Assume HLF: locally_finite_family X Tx Fam.

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

∎