:: deftheorem defines Tarski CLASSES1:def 2 :
for B being set holds
( B is Tarski iff ( B is subset-closed & ( for X being set st X in B holds
bool X in B ) & ( for X being set holds
( not X c= B or X,B are_equipotent or X in B ) ) ) );