for X being set holds
( GrothendieckUniverse X is Universe & ( for U being Universe st X in U holds
GrothendieckUniverse X c= U ) )