:: deftheorem GDef defines GrothendieckUniverse CLASSES3:def 5 :
for X being set
for b₂ being Grothendieck of X holds
( b₂ = GrothendieckUniverse X iff for G being Grothendieck of X holds b₂ c= G );