:: deftheorem defines SETS CLASSES2:def 3 :
SETS = Tarski-Class FinSETS;