Let X, Tx, C and D be given.

Assume Htop: topology_on X Tx.

Assume HC: closed_in X Tx C.

Assume HD: closed_in X Tx D.

We will prove closed_in X Tx (C ∪ D).

An exact proof term for the current goal is (closed_binunion X Tx C D HC HD).

∎