Let X, T and UFam be given.

Assume HTx: topology_on X T.

Assume HUFamPow: UFam ∈ 𝒫 T.

We will prove ⋃ UFam ∈ T.

We prove the intermediate claim HUFamSub: UFam ⊆ T.

An exact proof term for the current goal is (PowerE T UFam HUFamPow).

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

∎