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) `) ;
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) `)) ;
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) `)) ;
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))
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; :: thesis: verum