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 :: thesis: for A being Ordinal st A in card (Tarski-Class W) holds
succ A in card (Tarski-Class W)
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 Th13;
then succ A in Tarski-Class W by Th5;
then succ A in On (Tarski-Class W) by ORDINAL1:def 9;
hence succ A in card (Tarski-Class W) by Th9; :: thesis: verum
end;
hence card (Tarski-Class W) is limit_ordinal by ORDINAL1:28; :: thesis: verum