thus
G1 /\ G2 is epsilon-transitive
by CLASSES1:50; :: thesis: ( G1 /\ G2 is power-closed & G1 /\ G2 is FamUnion-closed )

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

hereby :: according to CLASSES3:def 1 :: thesis: G1 /\ G2 is FamUnion-closed

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 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;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

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