let T be TopSpace; :: thesis: for A, B being Subset of T st ( A is open or B is open ) holds
(Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))
let A, B be Subset of T; :: thesis: ( ( A is open or B is open ) implies (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) )
A1: Int (A ` ) misses (Int (A ` )) ` by XBOOLE_1:79;
A2: Int (B ` ) misses (Int (B ` )) ` by XBOOLE_1:79;
A /\ B misses (A /\ B) ` by XBOOLE_1:79;
then A3: {} T = (A /\ B) /\ ((A /\ B) ` ) by XBOOLE_0:def 7;
A4: (A /\ B) /\ (Int ((A /\ B) ` )) c= (A /\ B) /\ ((A /\ B) ` ) by TOPS_1:44, XBOOLE_1:26;
then A /\ (B /\ (Int ((A /\ B) ` ))) = {} T by A3, XBOOLE_1:16;
then A misses B /\ (Int ((A /\ B) ` )) by XBOOLE_0:def 7;
then B /\ (Int ((A /\ B) ` )) c= A ` by Th2;
then A5: Int (B /\ (Int ((A /\ B) ` ))) c= Int (A ` ) by TOPS_1:48;
B /\ (A /\ (Int ((A /\ B) ` ))) = {} T by A3, A4, XBOOLE_1:16;
then B misses A /\ (Int ((A /\ B) ` )) by XBOOLE_0:def 7;
then A /\ (Int ((A /\ B) ` )) c= B ` by Th2;
then A6: Int (A /\ (Int ((A /\ B) ` ))) c= Int (B ` ) by TOPS_1:48;
assume A7: ( A is open or B is open ) ; :: thesis: (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))

A8: now

per cases ( A is open or B is open ) by A7;

suppose A is open ; :: thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B))

then A /\ (Int ((A /\ B) ` )) c= ((Int (B ` )) ` ) ` by A6, TOPS_1:55;
then (Int (B ` )) ` misses A /\ (Int ((A /\ B) ` )) by Th2;
then ((Int (B ` )) ` ) /\ (A /\ (Int ((A /\ B) ` ))) = {} by XBOOLE_0:def 7;
then (((Cl ((B ` ) ` )) ` ) ` ) /\ (A /\ (Int ((A /\ B) ` ))) = {} by TOPS_1:def 1;
then A /\ ((Cl B) /\ (Int ((A /\ B) ` ))) = {} by XBOOLE_1:16;
then A misses (Cl B) /\ (Int ((A /\ B) ` )) by XBOOLE_0:def 7;
then (Cl B) /\ (Int ((A /\ B) ` )) c= A ` by Th2;
then Int ((Cl B) /\ (Int ((A /\ B) ` ))) c= Int (A ` ) by TOPS_1:48;
then (Int (Cl B)) /\ (Int (Int ((A /\ B) ` ))) c= Int (A ` ) by TOPS_1:46;
then ((Int (Cl B)) /\ (Int ((A /\ B) ` ))) /\ ((Int (A ` )) ` ) c= (Int (A ` )) /\ ((Int (A ` )) ` ) by XBOOLE_1:26;
then ((Int (Cl B)) /\ (Int ((A /\ B) ` ))) /\ ((Int (A ` )) ` ) c= {} T by A1, XBOOLE_0:def 7;
then ((Int (Cl B)) /\ (Int ((A /\ B) ` ))) /\ (((Cl ((A ` ) ` )) ` ) ` ) c= {} T by TOPS_1:def 1;
then {} T = (Int ((A /\ B) ` )) /\ ((Int (Cl B)) /\ (Cl A)) by XBOOLE_1:16;
then Int ((A /\ B) ` ) misses (Int (Cl B)) /\ (Cl A) by XBOOLE_0:def 7;
then (Int (Cl B)) /\ (Cl A) c= (Int ((A /\ B) ` )) ` by Th2;
then (Int (Cl B)) /\ (Cl A) c= ((Cl (((A /\ B) ` ) ` )) ` ) ` by TOPS_1:def 1;
then Int ((Int (Cl B)) /\ (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:48;
then (Int (Int (Cl B))) /\ (Int (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:46;
hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; :: thesis: verum

end;

suppose B is open ; :: thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B))

then B /\ (Int ((A /\ B) ` )) c= ((Int (A ` )) ` ) ` by A5, TOPS_1:55;
then (Int (A ` )) ` misses B /\ (Int ((A /\ B) ` )) by Th2;
then ((Int (A ` )) ` ) /\ (B /\ (Int ((A /\ B) ` ))) = {} T by XBOOLE_0:def 7;
then (((Cl ((A ` ) ` )) ` ) ` ) /\ (B /\ (Int ((A /\ B) ` ))) = {} T by TOPS_1:def 1;
then B /\ ((Cl A) /\ (Int ((A /\ B) ` ))) = {} T by XBOOLE_1:16;
then B misses (Cl A) /\ (Int ((A /\ B) ` )) by XBOOLE_0:def 7;
then (Cl A) /\ (Int ((A /\ B) ` )) c= B ` by Th2;
then Int ((Cl A) /\ (Int ((A /\ B) ` ))) c= Int (B ` ) by TOPS_1:48;
then (Int (Cl A)) /\ (Int (Int ((A /\ B) ` ))) c= Int (B ` ) by TOPS_1:46;
then ((Int (Cl A)) /\ (Int ((A /\ B) ` ))) /\ ((Int (B ` )) ` ) c= (Int (B ` )) /\ ((Int (B ` )) ` ) by XBOOLE_1:26;
then ((Int (Cl A)) /\ (Int ((A /\ B) ` ))) /\ ((Int (B ` )) ` ) c= {} T by A2, XBOOLE_0:def 7;
then ((Int (Cl A)) /\ (Int ((A /\ B) ` ))) /\ (((Cl ((B ` ) ` )) ` ) ` ) c= {} T by TOPS_1:def 1;
then {} T = (Int ((A /\ B) ` )) /\ ((Int (Cl A)) /\ (Cl B)) by XBOOLE_1:16;
then Int ((A /\ B) ` ) misses (Int (Cl A)) /\ (Cl B) by XBOOLE_0:def 7;
then (Int (Cl A)) /\ (Cl B) c= (Int ((A /\ B) ` )) ` by Th2;
then (Int (Cl A)) /\ (Cl B) c= ((Cl (((A /\ B) ` ) ` )) ` ) ` by TOPS_1:def 1;
then Int ((Int (Cl A)) /\ (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:48;
then (Int (Int (Cl A))) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:46;
hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; :: thesis: verum

end;

end;

end;

Cl (A /\ B) c= Cl B by PRE_TOPC:49, XBOOLE_1:17;
then A9: Int (Cl (A /\ B)) c= Int (Cl B) by TOPS_1:48;
Cl (A /\ B) c= Cl A by PRE_TOPC:49, XBOOLE_1:17;
then Int (Cl (A /\ B)) c= Int (Cl A) by TOPS_1:48;
then Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by A9, XBOOLE_1:19;
hence (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) by A8, XBOOLE_0:def 10; :: thesis: verum