Let X, T and UFam be given.

Assume HTx: topology_on X T.

Assume HUFam: UFam ⊆ T.

We will prove ⋃ UFam ∈ T.

We prove the intermediate claim H1: (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam0 ∈ 𝒫 T, ⋃ UFam0 ∈ T)) ∧ (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T).

An exact proof term for the current goal is HTx.

We prove the intermediate claim H2: ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam0 ∈ 𝒫 T, ⋃ UFam0 ∈ T).

An exact proof term for the current goal is (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam0 ∈ 𝒫 T, ⋃ UFam0 ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) H1).

We prove the intermediate claim HUnionAxiom: ∀UFam0 ∈ 𝒫 T, ⋃ UFam0 ∈ T.

An exact proof term for the current goal is (andER (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T)) (∀UFam0 ∈ 𝒫 T, ⋃ UFam0 ∈ T) H2).

We prove the intermediate claim HUFamPower: UFam ∈ 𝒫 T.

An exact proof term for the current goal is (PowerI T UFam HUFam).

An exact proof term for the current goal is (HUnionAxiom UFam HUFamPower).

∎