Let X and T be given.

Assume HTx: topology_on X T.

We will prove ∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T.

Let UFam be given.

Assume HUFamPow: UFam ∈ 𝒫 T.

An exact proof term for the current goal is (topology_union_closed_pow X T UFam HTx HUFamPow).

∎