let X be set ; :: thesis: ( GrothendieckUniverse X is Universe & ( for U being Universe st X in U holds
GrothendieckUniverse X c= U ) )
set G = GrothendieckUniverse X;
thus GrothendieckUniverse X is Universe by Def4; :: thesis: for U being Universe st X in U holds
GrothendieckUniverse X c= U
let U be Universe; :: thesis: ( X in U implies GrothendieckUniverse X c= U )
assume X in U ; :: thesis: GrothendieckUniverse X c= U
then U is Grothendieck of X by Def4;
hence GrothendieckUniverse X c= U by GDef; :: thesis: verum