set g = the Grothendieck of X;
defpred S₁[ 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 & S₁[Y] ) ) from XFAMILY:sch 1();
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 SETFAM_1:def 1, A4, A1;
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 A1, A6, SETFAM_1:def 1;
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 A8, A1, A7, SETFAM_1:def 1;
( rng f c= meet Gclasses & meet Gclasses c= Y ) by A8, A7, SETFAM_1:7;
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 SETFAM_1:3, A2, A1, XBOOLE_1:17;
then A11: ( M /\ G1 c= the Grothendieck of X & M /\ G1 c= G1 ) by XBOOLE_1:17;
then M c= M /\ G1 by A10, A1, SETFAM_1:3;
hence M c= G1 by A11; :: thesis: verum