theorem :: CLASSES5:38

for x being object ex U being Universe st x is U -set