Let X, Tx, Fam and U be given.
Assume HTx: topology_on X Tx.
Assume HFsubX: ∀A : set, A ∈ Fam → A ⊆ X.
Assume HLF: locally_finite_family X Tx Fam.
Assume HUopen: U ∈ Tx.
Assume HclSub: ∀A : set, A ∈ Fam → closure_of X Tx A ⊆ U.
We will prove closure_of X Tx (⋃ Fam) ⊆ U.
We prove the intermediate claim HclUsub: closure_of X Tx (⋃ Fam) ⊆ ⋃ {closure_of X Tx A|A ∈ Fam}.
An exact proof term for the current goal is (closure_Union_locally_finite_subset_Union_closures X Tx Fam HFsubX HLF).
Let x be given.
Assume Hxcl: x ∈ closure_of X Tx (⋃ Fam).
We will prove x ∈ U.
We prove the intermediate claim HxInUnionCl: x ∈ ⋃ {closure_of X Tx A|A ∈ Fam}.
An exact proof term for the current goal is (HclUsub x Hxcl).
Apply (UnionE_impred {closure_of X Tx A|A ∈ Fam} x HxInUnionCl (x ∈ U)) to the current goal.
Let C be given.
Assume HxC: x ∈ C.
Assume HC: C ∈ {closure_of X Tx A|A ∈ Fam}.
Apply (ReplE_impred Fam (λA0 : set ⇒ closure_of X Tx A0) C HC (x ∈ U)) to the current goal.
Let A be given.
Assume HAFam: A ∈ Fam.
Assume HCeq: C = closure_of X Tx A.
We prove the intermediate claim HxClA: x ∈ closure_of X Tx A.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is HxC.
An exact proof term for the current goal is (HclSub A HAFam x HxClA).
∎