let T be TopSpace; :: thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
let A, B be Subset of T; :: thesis: ( A is 1st_class & B is 1st_class implies ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) )
assume ( A is 1st_class & B is 1st_class ) ; :: thesis: ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
then A1: ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) & Int (Cl B) = Int (Cl (Int B)) & Cl (Int B) = Cl (Int (Cl B)) ) by Th51;
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:51, TOPS_1:48;
then A2: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:46;
A3: (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A1, Th1;
Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:49, TOPS_1:44;
then A4: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:48;
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:49, TOPS_1:49;
then A5: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:50;
A6: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A1, Th2;
Int (A \/ B) c= Int (Cl (A \/ B)) by PRE_TOPC:48, TOPS_1:48;
then Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:49;
hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A2, A3, A4, A5, A6, XBOOLE_0:def 10; :: thesis: verum