let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is closed_condensed & Q is closed_condensed holds
P \/ Q is closed_condensed
let P, Q be Subset of TS; :: thesis: ( P is closed_condensed & Q is closed_condensed implies P \/ Q is closed_condensed )
assume A1: ( P is closed_condensed & Q is closed_condensed ) ; :: thesis: P \/ Q is closed_condensed
then ( P = Cl (Int P) & Q = Cl (Int Q) ) by Def7;
then P \/ Q = Cl ((Int P) \/ (Int Q)) by PRE_TOPC:50;
then A2: P \/ Q c= Cl (Int (P \/ Q)) by Th49, PRE_TOPC:49;
A3: Cl (Int (P \/ Q)) c= Cl (P \/ Q) by Th44, PRE_TOPC:49;
( P is closed & Q is closed ) by A1, Th106;
then ( P = Cl P & Q = Cl Q ) by PRE_TOPC:52;
then Cl (Int (P \/ Q)) c= P \/ Q by A3, PRE_TOPC:50;
then P \/ Q = Cl (Int (P \/ Q)) by A2, XBOOLE_0:def 10;
hence P \/ Q is closed_condensed by Def7; :: thesis: verum