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

proof

(A /\ (Cl (Int B))) /\ B c= A /\ B by XBOOLE_1:17, XBOOLE_1:26;
then A /\ ((Cl (Int B)) /\ B) c= A /\ B by XBOOLE_1:16;
then Int (A /\ ((Cl (Int B)) /\ B)) c= Int (A /\ B) by TOPS_1:48;
then A2: Cl (Int (A /\ ((Cl (Int B)) /\ B))) c= Cl (Int (A /\ B)) by PRE_TOPC:49;
(Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ ((Cl (Int B)) /\ B))) by XBOOLE_1:17;
hence (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ B)) by A2, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: Cl (Int (A /\ B)) c= (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B))
A3: Cl (Int (A /\ ((Cl (Int B)) /\ B))) = Cl (Int ((A /\ (Cl (Int B))) /\ B)) by XBOOLE_1:16
.= Cl ((Int (A /\ (Cl (Int B)))) /\ (Int B)) by TOPS_1:46
.= Cl (((Int A) /\ (Int (Cl (Int B)))) /\ (Int B)) by TOPS_1:46
.= Cl ((Int A) /\ ((Int (Cl (Int B))) /\ (Int B))) by XBOOLE_1:16
.= Cl ((Int A) /\ (Int B)) by Th4, XBOOLE_1:28
.= Cl (Int (A /\ B)) by TOPS_1:46 ;
Int (A /\ B) c= Int B by TOPS_1:48, XBOOLE_1:17;
then Cl (Int (A /\ B)) c= Cl (Int B) by PRE_TOPC:49;
hence Cl (Int (A /\ B)) c= (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) by A3, XBOOLE_1:19; :: thesis: verum

end;

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