let U be Grothendieck; :: thesis: ( omega in U implies ( ( for x, u being set st x in u & u in U holds
x in U ) & ( for u, v being set st u in U & v in U holds
( {u,v} in U & [u,v] in U & [:u,v:] 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 ) ) )
assume A1: omega in U ; :: thesis: ( ( for x, u being set st x in u & u in U holds
x in U ) & ( for u, v being set st u in U & v in U holds
( {u,v} in U & [u,v] in U & [:u,v:] 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 ) )
then reconsider G = U as Universe ;

hereby :: thesis: ( ( for u, v being set st u in U & v in U holds
( {u,v} in U & [u,v] in U & [:u,v:] 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 ) )

let x, u be set ; :: thesis: ( x in u & u in U implies x in U )
assume A2: ( x in u & u in U ) ; :: thesis: x in U
U is axiom_GU1 ;
hence x in U by A2; :: thesis: verum

end;

hereby :: thesis: ( ( 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 ) )

let u, v be set ; :: thesis: ( u in U & v in U implies ( {u,v} in U & [u,v] in U & [:u,v:] in U ) )
assume that
A3: u in U and
A4: v in U ; :: thesis: ( {u,v} in U & [u,v] in U & [:u,v:] in U )
reconsider u9 = u, v9 = v as Element of G by A3, A4;
( {u9,v9} is Element of G & [u9,v9] is Element of G & [:u9,v9:] is Element of G ) ;
hence ( {u,v} in U & [u,v] in U & [:u,v:] in U ) ; :: thesis: verum

end;

hereby :: thesis: ( 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 ) )

let x be set ; :: thesis: ( x in U implies ( bool x in U & union x in U ) )
assume x in U ; :: thesis: ( bool x in U & union x in U )
then reconsider x9 = x as Element of G ;
( bool x9 in G & union x9 in G ) ;
hence ( bool x in U & union x in U ) ; :: thesis: verum

end;

thus omega in U by A1; :: thesis: 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
thus 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 by CLASSES3:2; :: thesis: verum