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:16, 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:19;
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:19;
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:23;
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:19;
then (Int (Cl B)) /\ (Int (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:17;
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:19;
then (Int (Int (Cl B))) /\ (Int (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:17;
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:23;
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:19;
then (Int (Cl A)) /\ (Int (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:17;
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:19;
then (Int (Int (Cl A))) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:17;
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:19, XBOOLE_1:17;
then A9: Int (Cl (A /\ B)) c= Int (Cl B) by TOPS_1:19;
Cl (A /\ B) c= Cl A by PRE_TOPC:19, XBOOLE_1:17;
then Int (Cl (A /\ B)) c= Int (Cl A) by TOPS_1:19;
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