let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is closed & Q is closed holds
P \/ Q is closed
let P, Q be Subset of TS; :: thesis: ( P is closed & Q is closed implies P \/ Q is closed )
assume ( P is closed & Q is closed ) ; :: thesis: P \/ Q is closed
then ( P = Cl P & Q = Cl Q ) by PRE_TOPC:52;
then Cl (P \/ Q) = P \/ Q by PRE_TOPC:50;
hence P \/ Q is closed ; :: thesis: verum