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)
Int (A /\ B) c= Int B by TOPS_1:19, XBOOLE_1:17;
then A1: Cl (Int (A /\ B)) c= Cl (Int B) by PRE_TOPC:19;
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:17
.= Cl (((Int A) /\ (Int (Cl (Int B)))) /\ (Int B)) by TOPS_1:17
.= 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:17 ;
then A2: Cl (Int (A /\ B)) c= (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) by A1, XBOOLE_1:19;
A /\ ((Cl (Int B)) /\ B) c= A /\ B by XBOOLE_1:17, XBOOLE_1:26;
then Int (A /\ ((Cl (Int B)) /\ B)) c= Int (A /\ B) by TOPS_1:19;
then A3: Cl (Int (A /\ ((Cl (Int B)) /\ B))) c= Cl (Int (A /\ B)) by PRE_TOPC:19;
(Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ ((Cl (Int B)) /\ B))) by XBOOLE_1:17;
then (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ B)) by A3;
then A4: (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) = Cl (Int (A /\ B)) by A2;
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 A4, XBOOLE_1:16; :: thesis: verum