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 A1: ( A is 1st_class & B is 1st_class ) ; :: thesis: ( A \/ B is 1st_class & A /\ B is 1st_class )
then A2: ( 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;
A3: Int (Cl (A /\ B)) = (Int (Cl A)) /\ (Int (Cl B)) by A1, Th53
.= Int (Cl (Int (A /\ B))) by A2, Th1 ;
Cl (Int (A \/ B)) = (Cl (Int A)) \/ (Cl (Int B)) by A1, Th53
.= Cl (Int (Cl (A \/ B))) by A2, Th2 ;
hence ( A \/ B is 1st_class & A /\ B is 1st_class ) by A3, Th52; :: thesis: verum