Let X, Tx and Fam be given.

Assume HTx: topology_on X Tx.

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

Assume HLF: locally_finite_family X Tx Fam.

Apply set_ext to the current goal.

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

An exact proof term for the current goal is (ex17_6c_closure_Union_contains_Union_closures X Tx Fam HTx HFsubX).

∎