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 A2, Th41;
Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;
then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A3, Th2;
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;
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 PRE_TOPC:18, TOPS_1:19;
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 PRE_TOPC:19, TOPS_1:20;
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 A2, Th41;
Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:19, TOPS_1:16;
then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19;
Int (Cl A) = Int (Cl (Int A)) by A1, Th41;
then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A8, Th1;
hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A5, A9, A7, A4, A6, XBOOLE_0:def 10; :: thesis: verum