Let X, Tx and Fam be given.

Assume Htop: topology_on X Tx.

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

We will prove ⋃ {closure_of X Tx A|A ∈ Fam} ⊆ closure_of X Tx (⋃ Fam).

Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.

We prove the intermediate claim HUnionSubX: ⋃ Fam ⊆ X.

Let x be given.

Assume Hx: x ∈ ⋃ Fam.

Apply (UnionE_impred Fam x Hx) to the current goal.

Let A be given.

Assume HxA.

Assume HAFam.

An exact proof term for the current goal is ((HFsub A HAFam) x HxA).

Let x be given.

Assume Hx: x ∈ ⋃ ClFam.

We will prove x ∈ closure_of X Tx (⋃ Fam).

Apply (UnionE_impred ClFam x Hx) to the current goal.

Let W be given.

Assume HxW.

Assume HWClFam.

Apply (ReplE Fam (λA : set ⇒ closure_of X Tx A) W HWClFam) to the current goal.

Let A be given.

Assume HAconj.

We prove the intermediate claim HAFam: A ∈ Fam.

An exact proof term for the current goal is (andEL (A ∈ Fam) (W = closure_of X Tx A) HAconj).

We prove the intermediate claim HWeq: W = closure_of X Tx A.

An exact proof term for the current goal is (andER (A ∈ Fam) (W = closure_of X Tx A) HAconj).

We prove the intermediate claim HxclA: x ∈ closure_of X Tx A.

rewrite the current goal using HWeq (from right to left).

An exact proof term for the current goal is HxW.

We prove the intermediate claim HASubUnion: A ⊆ ⋃ Fam.

Let y be given.

Assume Hy: y ∈ A.

An exact proof term for the current goal is (UnionI Fam y A Hy HAFam).

We prove the intermediate claim HxclUnion: x ∈ closure_of X Tx (⋃ Fam).

An exact proof term for the current goal is (closure_monotone X Tx A (⋃ Fam) Htop HASubUnion HUnionSubX x HxclA).

An exact proof term for the current goal is HxclUnion.

∎