:: deftheorem defines is_Tarski-Class_of CLASSES1:def 3 :
for A, B being set holds
( B is_Tarski-Class_of A iff ( A in B & B is Tarski ) );