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 that
A1: P is closed_condensed and
A2: Q is closed_condensed ; :: thesis: P \/ Q is closed_condensed
A3: Q = Cl (Int Q) by A2, Def7;
P = Cl (Int P) by A1, Def7;
then P \/ Q = Cl ((Int P) \/ (Int Q)) by A3, PRE_TOPC:20;
then A4: P \/ Q c= Cl (Int (P \/ Q)) by Th49, PRE_TOPC:19;
A5: Cl (Int (P \/ Q)) c= Cl (P \/ Q) by Th44, PRE_TOPC:19;
A6: Q is closed by A2, Th106;
P is closed by A1, Th106;
then Cl (Int (P \/ Q)) c= P \/ Q by A5, A6, PRE_TOPC:22;
then P \/ Q = Cl (Int (P \/ Q)) by A4, XBOOLE_0:def 10;
hence P \/ Q is closed_condensed by Def7; :: thesis: verum