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;
P = Cl (Int P) by A1;
then P \/ Q = Cl ((Int P) \/ (Int Q)) by A3, PRE_TOPC:20;
then A4: P \/ Q c= Cl (Int (P \/ Q)) by Th20, PRE_TOPC:19;
A5: Cl (Int (P \/ Q)) c= Cl (P \/ Q) by Th16, PRE_TOPC:19;
A6: Q is closed by A2;
P is closed by A1;
then Cl (Int (P \/ Q)) c= P \/ Q by A5, A6, PRE_TOPC:22;
then P \/ Q = Cl (Int (P \/ Q)) by A4;
hence P \/ Q is closed_condensed ; :: thesis: verum