let X, W be set ; :: thesis: ( W is Tarski & X in W implies card X in W )
assume that
A1: W is Tarski and
A2: X in W ; :: thesis: card X in W
A3: card W = On W by A1, Th9;
card X in card W by A1, A2, Th1;
hence card X in W by A3, ORDINAL1:def 9; :: thesis: verum