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 A1: 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 ) )
assume A2: B is condensed ; :: thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
then A3: B c= Cl (Int B) by TOPS_1:def 6;
A4: A c= Cl (Int A) by A1, 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);
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20;
then A5: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;
A \/ B c= (Cl (Int A)) \/ (Cl (Int B)) by A4, A3, XBOOLE_1:13;
then A \/ B c= Cl (Int (A \/ B)) by A5;
then A6: (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:19, TOPS_1:20;
then A7: (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:20;
Cl (Int (Cl (A \/ B))) c= Cl (Cl (A \/ B)) by PRE_TOPC:19, TOPS_1:16;
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:20;
then A8: Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7;
(Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) by PRE_TOPC:18, XBOOLE_1:9;
then (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A7;
then (Int (Cl (A \/ B))) \/ (A \/ B) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A6;
hence (Int (Cl (A \/ B))) \/ (A \/ B) is condensed by A8, TOPS_1:def 6; :: thesis: verum
end;
A9: Int (Cl B) c= B by A2, TOPS_1:def 6;
A10: Int (Cl A) c= A by A1, TOPS_1:def 6;
thus (Cl (Int (A /\ B))) /\ (A /\ B) is condensed :: thesis: verum
proof
set X = (Cl (Int (A /\ B))) /\ (A /\ B);
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;
then A11: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;
(Int (Cl A)) /\ (Int (Cl B)) c= A /\ B by A10, A9, XBOOLE_1:27;
then Int (Cl (A /\ B)) c= A /\ B by A11;
then A12: (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:21, TOPS_1:19;
then A13: Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) by TOPS_1:17;
Int (Int (A /\ B)) c= Int (Cl (Int (A /\ B))) by PRE_TOPC:18, TOPS_1:19;
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:17;
then A14: (Cl (Int (A /\ B))) /\ (A /\ B) c= Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by XBOOLE_1:17;
(Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by TOPS_1:16, XBOOLE_1:26;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by A13;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by A12;
hence (Cl (Int (A /\ B))) /\ (A /\ B) is condensed by A14, TOPS_1:def 6; :: thesis: verum
end;