let W, X be set ; :: thesis: ( W is Tarski & X in W implies card X in W )
assume A1: ( W is Tarski & X in W ) ; :: thesis: card X in W
( card X in card W & card W = On W ) by A1, Th1, Th10;
hence card X in W by ORDINAL1:def 10; :: thesis: verum