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 A1, XBOOLE_0:def 4;
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 A3, XBOOLE_0:def 4;
then A4: union (rng f) in G1 by A3, Def3;
( rng f c= G2 & X in G2 ) by A3, XBOOLE_0:def 4;
then union (rng f) in G2 by A3, Def3;
hence union (rng f) in G1 /\ G2 by A4, XBOOLE_0:def 4; :: thesis: verum