theorem :: CLASSES5:27

for U being Universe
for x being set st x is U -Class holds
not x is empty by CLASSES4:13;