Let X, T, U and V be given.

Assume HU: open_in X T U.

Assume HV: open_in X T V.

We will prove open_in X T (U ∪ V).

We prove the intermediate claim HTx: topology_on X T.

An exact proof term for the current goal is (andEL (topology_on X T) (U ∈ T) HU).

We prove the intermediate claim HUinT: U ∈ T.

An exact proof term for the current goal is (andER (topology_on X T) (U ∈ T) HU).

We prove the intermediate claim HVinT: V ∈ T.

An exact proof term for the current goal is (andER (topology_on X T) (V ∈ T) HV).

We will prove topology_on X T ∧ (U ∪ V) ∈ T.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is (topology_binunion_closed X T U V HTx HUinT HVinT).

∎