Let X, T and UFam be given.
Assume HTx: topology_on X T.
Assume HUFam: ∀U ∈ UFam, open_in X T U.
We will prove open_in X T (⋃ UFam).
We will prove topology_on X T ∧ ⋃ UFam ∈ T.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We will prove ⋃ UFam ∈ T.
We prove the intermediate claim HUFamsub: UFam ⊆ T.
Let U be given.
Assume HUin: U ∈ UFam.
We prove the intermediate claim HUopen: open_in X T U.
An exact proof term for the current goal is (HUFam U HUin).
An exact proof term for the current goal is (andER (topology_on X T) (U ∈ T) HUopen).
An exact proof term for the current goal is (topology_union_closed X T UFam HTx HUFamsub).
∎