theorem :: CLASSES5:39

for x being set holds x is GrothendieckUniverse x -set by CLASSES3:def 4;