theorem Th5: :: CLASSES1:5

for X, Y being set holds
( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )