let T be TopSpace; :: thesis: for A, B being Subset of T st A is condensed & B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
let A, B be Subset of T; :: thesis: ( A is condensed & B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) )
assume A is condensed ; :: thesis: ( not B is condensed or ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) )
then A1: ( Int (Cl A) c= A & A c= Cl (Int A) ) by TOPS_1:def 6;
assume B is condensed ; :: thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
then A2: ( Int (Cl B) c= B & B c= Cl (Int B) ) by TOPS_1:def 6;
thus (Int (Cl (A \/ B))) \/ (A \/ B) is condensed :: thesis: (Cl (Int (A /\ B))) /\ (A /\ B) is condensed

proof

set X = (Int (Cl (A \/ B))) \/ (A \/ B);
A3: (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) by PRE_TOPC:48, XBOOLE_1:9;
A4: A \/ B c= (Cl (Int A)) \/ (Cl (Int B)) by A1, A2, XBOOLE_1:13;
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:49, TOPS_1:49;
then (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:50;
then A \/ B c= Cl (Int (A \/ B)) by A4, XBOOLE_1:1;
then A5: (Int (Cl (A \/ B))) \/ (A \/ B) c= (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) by XBOOLE_1:9;
Cl ((Int (Int (Cl (A \/ B)))) \/ (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:49, TOPS_1:49;
then (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:50;
then (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A3, XBOOLE_1:1;
then A6: (Int (Cl (A \/ B))) \/ (A \/ B) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A5, XBOOLE_1:1;
Cl (Int (Cl (A \/ B))) c= Cl (Cl (A \/ B)) by PRE_TOPC:49, TOPS_1:44;
then (Cl (Int (Cl (A \/ B)))) \/ (Cl (A \/ B)) = Cl (A \/ B) by XBOOLE_1:12;
then Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) = Int (Cl (A \/ B)) by PRE_TOPC:50;
then Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7;
hence (Int (Cl (A \/ B))) \/ (A \/ B) is condensed by A6, TOPS_1:def 6; :: thesis: verum

end;

thus (Cl (Int (A /\ B))) /\ (A /\ B) is condensed :: thesis: verum

proof

set X = (Cl (Int (A /\ B))) /\ (A /\ B);
A7: (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by TOPS_1:44, XBOOLE_1:26;
A8: (Int (Cl A)) /\ (Int (Cl B)) c= A /\ B by A1, A2, XBOOLE_1:27;
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:51, TOPS_1:48;
then Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:46;
then Int (Cl (A /\ B)) c= A /\ B by A8, XBOOLE_1:1;
then A9: (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by XBOOLE_1:26;
Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= Int ((Cl (Cl (Int (A /\ B)))) /\ (Cl (A /\ B))) by PRE_TOPC:51, TOPS_1:48;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) by TOPS_1:46;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by A7, XBOOLE_1:1;
then A10: Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by A9, XBOOLE_1:1;
Int (Int (A /\ B)) c= Int (Cl (Int (A /\ B))) by PRE_TOPC:48, TOPS_1:48;
then Int (A /\ B) = (Int (Cl (Int (A /\ B)))) /\ (Int (A /\ B)) by XBOOLE_1:28;
then Cl (Int (A /\ B)) = Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by TOPS_1:46;
then (Cl (Int (A /\ B))) /\ (A /\ B) c= Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by XBOOLE_1:17;
hence (Cl (Int (A /\ B))) /\ (A /\ B) is condensed by A10, TOPS_1:def 6; :: thesis: verum

end;