theorem :: CLASSES2:20

for W being set st W is Tarski & W <> {} holds
( card W <> 0 & card W <> {} & card W is limit_ordinal ) by Th19;