theorem :: CLASSES5:35

for U being Universe
for x being object holds
( not x is U -Class or not x is U -set ) ;