:: deftheorem defines -set CLASSES5:def 8 :
for X being non empty set
for x being object holds
( x is X -set iff x in X );