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

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