set g = the Grothendieck of X;
defpred S1[ set ] means \$1 is Grothendieck of X;
consider Gclasses being set such that
A1: for Y being set holds
( Y in Gclasses iff ( Y in bool the Grothendieck of X & S1[Y] ) ) from A2: the Grothendieck of X in bool the Grothendieck of X by ZFMISC_1:def 1;
then reconsider Gclasses = Gclasses as non empty set by A1;
set M = meet Gclasses;
A3: meet Gclasses is epsilon-transitive
proof
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in meet Gclasses or Y c= meet Gclasses )
assume A4: Y in meet Gclasses ; :: thesis: Y c= meet Gclasses
for Z being set st Z in Gclasses holds
Y c= Z
proof
let Z be set ; :: thesis: ( Z in Gclasses implies Y c= Z )
assume Z in Gclasses ; :: thesis: Y c= Z
then ( Y in Z & Z is epsilon-transitive ) by ;
hence Y c= Z ; :: thesis: verum
end;
hence Y c= meet Gclasses by SETFAM_1:5; :: thesis: verum
end;
A5: meet Gclasses is power-closed
proof
let Z be set ; :: according to CLASSES3:def 1 :: thesis: ( Z in meet Gclasses implies bool Z in meet Gclasses )
assume A6: Z in meet Gclasses ; :: thesis: bool Z in meet Gclasses
for Y being set st Y in Gclasses holds
bool Z in Y
proof
let Y be set ; :: thesis: ( Y in Gclasses implies bool Z in Y )
assume Y in Gclasses ; :: thesis: bool Z in Y
then ( Z in Y & Y is power-closed ) by ;
hence bool Z in Y ; :: thesis: verum
end;
hence bool Z in meet Gclasses by SETFAM_1:def 1; :: thesis: verum
end;
meet Gclasses is FamUnion-closed
proof
let Z be set ; :: according to CLASSES3:def 3 :: thesis: for f being Function st dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses holds
union (rng f) in meet Gclasses

let f be Function; :: thesis: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses implies union (rng f) in meet Gclasses )
assume A7: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses ) ; :: thesis: union (rng f) in meet Gclasses
for Y being set st Y in Gclasses holds
union (rng f) in Y
proof
let Y be set ; :: thesis: ( Y in Gclasses implies union (rng f) in Y )
assume A8: Y in Gclasses ; :: thesis: union (rng f) in Y
A9: ( Z in Y & Y is FamUnion-closed ) by ;
( rng f c= meet Gclasses & meet Gclasses c= Y ) by ;
then rng f c= Y ;
hence union (rng f) in Y by A7, A9; :: thesis: verum
end;
hence union (rng f) in meet Gclasses by SETFAM_1:def 1; :: thesis: verum
end;
then reconsider M = meet Gclasses as Grothendieck by A3, A5;
M is Grothendieck of X
proof
now :: thesis: for Y being set st Y in Gclasses holds
X in Y
let Y be set ; :: thesis: ( Y in Gclasses implies X in Y )
assume Y in Gclasses ; :: thesis: X in Y
then Y is Grothendieck of X by A1;
hence X in Y by Def4; :: thesis: verum
end;
hence X in M by SETFAM_1:def 1; :: according to CLASSES3:def 4 :: thesis: verum
end;
then reconsider M = M as Grothendieck of X ;
take M ; :: thesis: for G being Grothendieck of X holds M c= G
let G1 be Grothendieck of X; :: thesis: M c= G1
A10: M /\ G1 is Grothendieck of X by Th1;
( M /\ G1 c= M & M c= the Grothendieck of X ) by ;
then A11: ( M /\ G1 c= the Grothendieck of X & M /\ G1 c= G1 ) by XBOOLE_1:17;
then M c= M /\ G1 by ;
hence M c= G1 by A11; :: thesis: verum