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 that
A1: A is 1st_class and
A2: 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)) )
A3: Cl (Int B) = Cl (Int (Cl B)) by ;
Cl (Int A) = Cl (Int (Cl A)) by ;
then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by ;
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by ;
then A5: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;
Int (A \/ B) c= Int (Cl (A \/ B)) by ;
then A6: Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:19;
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by ;
then A7: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;
A8: Int (Cl B) = Int (Cl (Int B)) by ;
Cl (Int (A /\ B)) c= Cl (A /\ B) by ;
then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19;
Int (Cl A) = Int (Cl (Int A)) by ;
then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by ;
hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by ; :: thesis: verum