theorem :: CLASSES4:7

for X being set holds
( X is Universe iff X is non empty Grothendieck ) ;