let T be TopSpace; :: thesis: for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds
Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
let A, B, C be Subset of T; :: thesis: ( A is closed_condensed & B is closed_condensed & C is closed_condensed implies Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) )
assume ( A is closed_condensed & B is closed_condensed & C is closed_condensed ) ; :: thesis: Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
then A1: ( A = Cl (Int A) & B = Cl (Int B) & C = Cl (Int C) ) by TOPS_1:def 7;
Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:46;
then Cl (Int (A /\ B)) c= A /\ B by A1, PRE_TOPC:51;
then ( Int ((Cl (Int (A /\ B))) /\ C) c= (Cl (Int (A /\ B))) /\ C & (Cl (Int (A /\ B))) /\ C c= (A /\ B) /\ C ) by TOPS_1:44, XBOOLE_1:26;
then A2: Int ((Cl (Int (A /\ B))) /\ C) c= (A /\ B) /\ C by XBOOLE_1:1;
then ( Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) & A /\ (B /\ C) c= B /\ C ) by XBOOLE_1:16, XBOOLE_1:17;
then Int ((Cl (Int (A /\ B))) /\ C) c= B /\ C by XBOOLE_1:1;
then Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (B /\ C) by TOPS_1:48;
then ( Int ((Cl (Int (A /\ B))) /\ C) c= Int (B /\ C) & Int (B /\ C) c= Cl (Int (B /\ C)) ) by PRE_TOPC:48;
then A3: Int ((Cl (Int (A /\ B))) /\ C) c= Cl (Int (B /\ C)) by XBOOLE_1:1;
( Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) & A /\ (B /\ C) c= A ) by A2, XBOOLE_1:16, XBOOLE_1:17;
then Int ((Cl (Int (A /\ B))) /\ C) c= A by XBOOLE_1:1;
then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (Cl (Int (B /\ C))) by A3, XBOOLE_1:19;
then Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (A /\ (Cl (Int (B /\ C)))) by TOPS_1:48;
then A4: Cl (Int ((Cl (Int (A /\ B))) /\ C)) c= Cl (Int (A /\ (Cl (Int (B /\ C))))) by PRE_TOPC:49;
Cl (Int (B /\ C)) = Cl ((Int B) /\ (Int C)) by TOPS_1:46;
then Cl (Int (B /\ C)) c= B /\ C by A1, PRE_TOPC:51;
then ( Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (Cl (Int (B /\ C))) & A /\ (Cl (Int (B /\ C))) c= A /\ (B /\ C) ) by TOPS_1:44, XBOOLE_1:26;
then A5: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (B /\ C) by XBOOLE_1:1;
then ( Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C & (A /\ B) /\ C c= A /\ B ) by XBOOLE_1:16, XBOOLE_1:17;
then Int (A /\ (Cl (Int (B /\ C)))) c= A /\ B by XBOOLE_1:1;
then Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int (A /\ B) by TOPS_1:48;
then ( Int (A /\ (Cl (Int (B /\ C)))) c= Int (A /\ B) & Int (A /\ B) c= Cl (Int (A /\ B)) ) by PRE_TOPC:48;
then A6: Int (A /\ (Cl (Int (B /\ C)))) c= Cl (Int (A /\ B)) by XBOOLE_1:1;
( Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C & (A /\ B) /\ C c= C ) by A5, XBOOLE_1:16, XBOOLE_1:17;
then Int (A /\ (Cl (Int (B /\ C)))) c= C by XBOOLE_1:1;
then Int (A /\ (Cl (Int (B /\ C)))) c= (Cl (Int (A /\ B))) /\ C by A6, XBOOLE_1:19;
then Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int ((Cl (Int (A /\ B))) /\ C) by TOPS_1:48;
then Cl (Int (A /\ (Cl (Int (B /\ C))))) c= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by PRE_TOPC:49;
hence Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A4, XBOOLE_0:def 10; :: thesis: verum