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

( 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