thus G1 /\ G2 is epsilon-transitive by CLASSES1:50; :: thesis: ( G1 /\ G2 is power-closed & G1 /\ G2 is FamUnion-closed )
hereby :: according to CLASSES3:def 1 :: thesis: G1 /\ G2 is FamUnion-closed
let X be set ; :: thesis: ( X in G1 /\ G2 implies bool X in G1 /\ G2 )
assume A1: X in G1 /\ G2 ; :: thesis: bool X in G1 /\ G2
A2: ( G1 is power-closed & G2 is power-closed ) ;
( X in G1 & X in G2 ) by ;
then ( bool X in G1 & bool X in G2 ) by A2;
hence bool X in G1 /\ G2 by XBOOLE_0:def 4; :: thesis: verum
end;
let X be set ; :: according to CLASSES3:def 3 :: thesis: for f being Function st dom f = X & rng f c= G1 /\ G2 & X in G1 /\ G2 holds
union (rng f) in G1 /\ G2

let f be Function; :: thesis: ( dom f = X & rng f c= G1 /\ G2 & X in G1 /\ G2 implies union (rng f) in G1 /\ G2 )
assume A3: ( dom f = X & rng f c= G1 /\ G2 & X in G1 /\ G2 ) ; :: thesis: union (rng f) in G1 /\ G2
( rng f c= G1 & X in G1 ) by ;
then A4: union (rng f) in G1 by ;
( rng f c= G2 & X in G2 ) by ;
then union (rng f) in G2 by ;
hence union (rng f) in G1 /\ G2 by ; :: thesis: verum