let W be set ; :: thesis: ( W is Tarski implies card W is limit_ordinal )
assume A1: W is Tarski ; :: thesis: card W is limit_ordinal

now :: thesis: for A being Ordinal st A in card W holds
succ A in card W

let A be Ordinal; :: thesis: ( A in card W implies succ A in card W )
assume A in card W ; :: thesis: succ A in card W
then A in W by A1, Th13;
then succ A in W by A1, Th5;
then succ A in On W by ORDINAL1:def 9;
hence succ A in card W by A1, Th9; :: thesis: verum

end;

hence card W is limit_ordinal by ORDINAL1:28; :: thesis: verum