:: deftheorem Def4 defines Tarski-Class CLASSES1:def 4 :
for A, b₂ being set holds
( b₂ = Tarski-Class A iff ( b₂ is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b₂ c= D ) ) );