let W be set ; :: thesis: ( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )
thus card (Tarski-Class W) <> 0 ; :: thesis: ( card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )
thus card (Tarski-Class W) <> {} ; :: thesis: card (Tarski-Class W) is limit_ordinal

now

let A be Ordinal; :: thesis: ( A in card (Tarski-Class W) implies succ A in card (Tarski-Class W) )
assume A in card (Tarski-Class W) ; :: thesis: succ A in card (Tarski-Class W)
then A in Tarski-Class W by Th14;
then succ A in Tarski-Class W by Th6;
then succ A in On (Tarski-Class W) by ORDINAL1:def 10;
hence succ A in card (Tarski-Class W) by Th10; :: thesis: verum

end;

hence card (Tarski-Class W) is limit_ordinal by ORDINAL1:41; :: thesis: verum