Let X and UFam be given.

Assume HUFam: UFam ∈ 𝒫 (countable_complement_topology X).

We will prove ⋃ UFam ∈ countable_complement_topology X.

We prove the intermediate claim Htop: topology_on X (countable_complement_topology X).

An exact proof term for the current goal is (countable_complement_topology_on X).

An exact proof term for the current goal is (topology_union_axiom X (countable_complement_topology X) Htop UFam HUFam).

∎