let T be TopSpace; :: thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( A \/ B is 1st_class & A /\ B is 1st_class )
let A, B be Subset of T; :: thesis: ( A is 1st_class & B is 1st_class implies ( A \/ B is 1st_class & A /\ B is 1st_class ) )
assume that
A1: A is 1st_class and
A2: B is 1st_class ; :: thesis: ( A \/ B is 1st_class & A /\ B is 1st_class )
A3: Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;
A4: Int (Cl B) = Int (Cl (Int B)) by A2, Th41;
A5: Int (Cl A) = Int (Cl (Int A)) by A1, Th41;
A6: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41;
A7: Cl (Int (A \/ B)) = (Cl (Int A)) \/ (Cl (Int B)) by A1, A2, Th43
.= Cl (Int (Cl (A \/ B))) by A3, A6, Th2 ;
Int (Cl (A /\ B)) = (Int (Cl A)) /\ (Int (Cl B)) by A1, A2, Th43
.= Int (Cl (Int (A /\ B))) by A5, A4, Th1 ;
hence ( A \/ B is 1st_class & A /\ B is 1st_class ) by A7, Th42; :: thesis: verum