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 that
A1: A is closed_condensed and
A2: B is closed_condensed and
A3: C is closed_condensed ; :: thesis: Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
A4: B = Cl (Int B) by A2, TOPS_1:def 7;
A5: (A /\ B) /\ C c= C by XBOOLE_1:17;
A6: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (Cl (Int (B /\ C))) by TOPS_1:44;
A7: Cl (Int (B /\ C)) = Cl ((Int B) /\ (Int C)) by TOPS_1:46;
C = Cl (Int C) by A3, TOPS_1:def 7;
then A /\ (Cl (Int (B /\ C))) c= A /\ (B /\ C) by A7, A4, PRE_TOPC:51, XBOOLE_1:26;
then A8: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (B /\ C) by A6, XBOOLE_1:1;
then Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by XBOOLE_1:16;
then A9: Int (A /\ (Cl (Int (B /\ C)))) c= C by A5, XBOOLE_1:1;
A10: (A /\ B) /\ C c= A /\ B by XBOOLE_1:17;
Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by A8, XBOOLE_1:16;
then Int (A /\ (Cl (Int (B /\ C)))) c= A /\ B by A10, XBOOLE_1:1;
then A11: Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int (A /\ B) by TOPS_1:48;
Int (A /\ B) c= Cl (Int (A /\ B)) by PRE_TOPC:48;
then Int (A /\ (Cl (Int (B /\ C)))) c= Cl (Int (A /\ B)) by A11, XBOOLE_1:1;
then Int (A /\ (Cl (Int (B /\ C)))) c= (Cl (Int (A /\ B))) /\ C by A9, XBOOLE_1:19;
then Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int ((Cl (Int (A /\ B))) /\ C) by TOPS_1:48;
then A12: Cl (Int (A /\ (Cl (Int (B /\ C))))) c= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by PRE_TOPC:49;
A13: A /\ (B /\ C) c= B /\ C by XBOOLE_1:17;
A14: A /\ (B /\ C) c= A by XBOOLE_1:17;
A15: Int ((Cl (Int (A /\ B))) /\ C) c= (Cl (Int (A /\ B))) /\ C by TOPS_1:44;
A16: Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:46;
A = Cl (Int A) by A1, TOPS_1:def 7;
then (Cl (Int (A /\ B))) /\ C c= (A /\ B) /\ C by A16, A4, PRE_TOPC:51, XBOOLE_1:26;
then A17: Int ((Cl (Int (A /\ B))) /\ C) c= (A /\ B) /\ C by A15, XBOOLE_1:1;
then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by XBOOLE_1:16;
then A18: Int ((Cl (Int (A /\ B))) /\ C) c= A by A14, XBOOLE_1:1;
Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by A17, XBOOLE_1:16;
then Int ((Cl (Int (A /\ B))) /\ C) c= B /\ C by A13, XBOOLE_1:1;
then A19: Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (B /\ C) by TOPS_1:48;
Int (B /\ C) c= Cl (Int (B /\ C)) by PRE_TOPC:48;
then Int ((Cl (Int (A /\ B))) /\ C) c= Cl (Int (B /\ C)) by A19, XBOOLE_1:1;
then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (Cl (Int (B /\ C))) by A18, XBOOLE_1:19;
then Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (A /\ (Cl (Int (B /\ C)))) by TOPS_1:48;
then Cl (Int ((Cl (Int (A /\ B))) /\ C)) c= Cl (Int (A /\ (Cl (Int (B /\ C))))) by PRE_TOPC:49;
hence Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A12, XBOOLE_0:def 10; :: thesis: verum