Let X, T, U and V be given.

Assume HTx: topology_on X T.

Assume HU: U ∈ T.

Assume HV: V ∈ T.

We will prove U ∪ V ∈ T.

We prove the intermediate claim Hpairsub: {U,V} ⊆ T.

Let W be given.

Assume HW: W ∈ {U,V}.

We prove the intermediate claim Hor: W = U ∨ W = V.

An exact proof term for the current goal is (UPairE W U V HW).

Apply Hor to the current goal.

Assume HWU: W = U.

rewrite the current goal using HWU (from left to right).

An exact proof term for the current goal is HU.

Assume HWV: W = V.

rewrite the current goal using HWV (from left to right).

An exact proof term for the current goal is HV.

We prove the intermediate claim HUnionPair: ⋃ {U,V} ∈ T.

An exact proof term for the current goal is (topology_union_closed X T {U,V} HTx Hpairsub).

rewrite the current goal using (binunion_eq_Union_pair U V) (from left to right).

An exact proof term for the current goal is HUnionPair.

∎