let U be set ; :: thesis: ( ( for x, u being set st x in u & u in U holds
x in U ) & ( for x being set st x in U holds
( bool x in U & union x in U ) ) & omega in U & ( for a, b being set
for f being Function of a,b st dom f = a & f is onto & a in U & b c= U holds
b in U ) implies U is Grothendieck )
assume that
A1: for x, u being set st x in u & u in U holds
x in U and
A2: for x being set st x in U holds
( bool x in U & union x in U ) and
A3: omega in U and
A4: for a, b being set
for f being Function of a,b st dom f = a & f is onto & a in U & b c= U holds
b in U ; :: thesis: U is Grothendieck
reconsider U9 = U as non empty set by A3;

now :: thesis: ( U is axiom_GU1 & U is axiom_GU3 & U9 is axiom_GU4 )

thus U is axiom_GU1 by A1; :: thesis: ( U is axiom_GU3 & U9 is axiom_GU4 )
thus U is axiom_GU3 by A2; :: thesis: U9 is axiom_GU4

now :: thesis: for Y being set
for f being Function st dom f = Y & rng f c= U9 & Y in U9 holds
union (rng f) in U9

let Y be set ; :: thesis: for f being Function st dom f = Y & rng f c= U9 & Y in U9 holds
union (rng f) in U9
let f be Function; :: thesis: ( dom f = Y & rng f c= U9 & Y in U9 implies union (rng f) in U9 )
assume that
A5: dom f = Y and
A6: rng f c= U9 and
A7: Y in U9 ; :: thesis: union (rng f) in U9
reconsider f9 = f as Function of Y,(rng f) by A5, FUNCT_2:1;
f9 is onto ;
then rng f9 in U9 by A5, A6, A7, A4;
hence union (rng f) in U9 by A2; :: thesis: verum

end;

then U9 is FamUnion-closed ;
hence U9 is axiom_GU4 by Th4; :: thesis: verum

end;

hence U is Grothendieck by Th3, Th4, CLASSES3:def 1; :: thesis: verum