:: deftheorem defines FinSETS CLASSES2:def 2 :
FinSETS = Tarski-Class {};