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