let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds
P /\ Q is open_condensed
let P, Q be Subset of TS; :: thesis: ( P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed )
A1: (P `) \/ (Q `) = (P /\ Q) ` by XBOOLE_1:54;
assume that
A2: P is open_condensed and
A3: Q is open_condensed ; :: thesis: P /\ Q is open_condensed
A4: Q ` is closed_condensed by A3;
P ` is closed_condensed by A2;
then (P `) \/ (Q `) is closed_condensed by A4, Th68;
hence P /\ Q is open_condensed by A1; :: thesis: verum