let T be TopSpace; :: thesis: for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)
let A, B be Subset of T; :: thesis: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)
A1: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) = Int (Cl (A \/ B))

proof

A2: Int (Cl (A \/ ((Int (Cl B)) \/ B))) = Int (Cl ((A \/ (Int (Cl B))) \/ B)) by XBOOLE_1:4
.= Int ((Cl (A \/ (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:50
.= Int (((Cl A) \/ (Cl (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:50
.= Int ((Cl A) \/ ((Cl (Int (Cl B))) \/ (Cl B))) by XBOOLE_1:4
.= Int ((Cl A) \/ (Cl B)) by Th3, XBOOLE_1:12
.= Int (Cl (A \/ B)) by PRE_TOPC:50 ;
Cl B c= Cl (A \/ B) by PRE_TOPC:49, XBOOLE_1:7;
then Int (Cl B) c= Int (Cl (A \/ B)) by TOPS_1:48;
hence (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) c= Int (Cl (A \/ B)) by A2, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: Int (Cl (A \/ B)) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B))
A \/ B c= (A \/ (Int (Cl B))) \/ B by XBOOLE_1:7, XBOOLE_1:9;
then A \/ B c= A \/ ((Int (Cl B)) \/ B) by XBOOLE_1:4;
then Cl (A \/ B) c= Cl (A \/ ((Int (Cl B)) \/ B)) by PRE_TOPC:49;
then A3: Int (Cl (A \/ B)) c= Int (Cl (A \/ ((Int (Cl B)) \/ B))) by TOPS_1:48;
Int (Cl (A \/ ((Int (Cl B)) \/ B))) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by XBOOLE_1:7;
hence Int (Cl (A \/ B)) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by A3, XBOOLE_1:1; :: thesis: verum

end;

A \/ ((Int (Cl B)) \/ B) = (Int (Cl B)) \/ (A \/ B) by XBOOLE_1:4;
hence (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) by A1, XBOOLE_1:4; :: thesis: verum