Let X, T, U and V be given.
Assume HT: topology_on X T.
Assume HU: U ∈ T.
Assume HV: V ∈ T.
We will prove U ∪ V ∈ T.
We prove the intermediate claim HUFamSub: UPair U V ⊆ T.
Let W be given.
Assume HW: W ∈ UPair U V.
Apply (UPairE W U V HW) to the current goal.
Assume HWeqU.
rewrite the current goal using HWeqU (from left to right).
An exact proof term for the current goal is HU.
Assume HWeqV.
rewrite the current goal using HWeqV (from left to right).
An exact proof term for the current goal is HV.
We prove the intermediate claim HUnion: ⋃ (UPair U V) ∈ T.
An exact proof term for the current goal is (topology_union_closed X T (UPair U V) HT HUFamSub).
rewrite the current goal using (Union_UPair_eq_binunion U V) (from right to left).
An exact proof term for the current goal is HUnion.
∎