:: deftheorem defines -Class CLASSES5:def 10 :
for U being Universe
for x being object holds
( x is U -Class iff ( x in bool U & not x in U ) );