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 that
A1: A is open_condensed and
A2: B is open_condensed and
A3: C is open_condensed ; :: thesis: Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C))
A4: B = Int (Cl B) by A2, TOPS_1:def 8;
A5: C c= (A \/ B) \/ C by XBOOLE_1:7;
A6: A \/ (Int (Cl (B \/ C))) c= Cl (A \/ (Int (Cl (B \/ C)))) by PRE_TOPC:18;
A7: Int (Cl (B \/ C)) = Int ((Cl B) \/ (Cl C)) by PRE_TOPC:20;
C = Int (Cl C) by A3, TOPS_1:def 8;
then A \/ (B \/ C) c= A \/ (Int (Cl (B \/ C))) by A7, A4, TOPS_1:20, XBOOLE_1:9;
then A8: A \/ (B \/ C) c= Cl (A \/ (Int (Cl (B \/ C)))) by A6;
then (A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by XBOOLE_1:4;
then A9: C c= Cl (A \/ (Int (Cl (B \/ C)))) by A5;
A10: A \/ B c= (A \/ B) \/ C by XBOOLE_1:7;
(A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A8, XBOOLE_1:4;
then A \/ B c= Cl (A \/ (Int (Cl (B \/ C)))) by A10;
then A11: Cl (A \/ B) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19;
Int (Cl (A \/ B)) c= Cl (A \/ B) by TOPS_1:16;
then Int (Cl (A \/ B)) c= Cl (A \/ (Int (Cl (B \/ C)))) by A11;
then (Int (Cl (A \/ B))) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A9, XBOOLE_1:8;
then Cl ((Int (Cl (A \/ B))) \/ C) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19;
then A12: Int (Cl ((Int (Cl (A \/ B))) \/ C)) c= Int (Cl (A \/ (Int (Cl (B \/ C))))) by TOPS_1:19;
A13: B \/ C c= A \/ (B \/ C) by XBOOLE_1:7;
A14: A c= A \/ (B \/ C) by XBOOLE_1:7;
A15: (Int (Cl (A \/ B))) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by PRE_TOPC:18;
A16: Int (Cl (A \/ B)) = Int ((Cl A) \/ (Cl B)) by PRE_TOPC:20;
A = Int (Cl A) by A1, TOPS_1:def 8;
then (A \/ B) \/ C c= (Int (Cl (A \/ B))) \/ C by A16, A4, TOPS_1:20, XBOOLE_1:9;
then A17: (A \/ B) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A15;
then A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by XBOOLE_1:4;
then A18: A c= Cl ((Int (Cl (A \/ B))) \/ C) by A14;
A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by A17, XBOOLE_1:4;
then B \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A13;
then A19: Cl (B \/ C) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19;
Int (Cl (B \/ C)) c= Cl (B \/ C) by TOPS_1:16;
then Int (Cl (B \/ C)) c= Cl ((Int (Cl (A \/ B))) \/ C) by A19;
then A \/ (Int (Cl (B \/ C))) c= Cl ((Int (Cl (A \/ B))) \/ C) by A18, XBOOLE_1:8;
then Cl (A \/ (Int (Cl (B \/ C)))) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19;
then Int (Cl (A \/ (Int (Cl (B \/ C))))) c= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by TOPS_1:19;
hence Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A12; :: thesis: verum