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

now

let X be set ; :: thesis: ( X in On W implies ( X is Ordinal & X c= On W ) )
assume A2: X in On W ; :: thesis: ( X is Ordinal & X c= On W )
hence X is Ordinal by ORDINAL1:def 10; :: thesis: X c= On W
reconsider A = X as Ordinal by A2, ORDINAL1:def 10;
A3: X in W by A2, ORDINAL1:def 10;
thus X c= On W :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in On W )
assume A4: x in X ; :: thesis: x in On W
then x in A ;
then reconsider B = x as Ordinal ;
B c= A by A4, ORDINAL1:def 2;
then B in W by A1, A3, CLASSES1:def 1;
hence x in On W by ORDINAL1:def 10; :: thesis: verum

end;

end;

then reconsider ON = On W as Ordinal by ORDINAL1:31;

A5: now

assume ON in W ; :: thesis: contradiction
then ON in ON by ORDINAL1:def 10;
hence contradiction ; :: thesis: verum

end;

ON c= W by ORDINAL2:9;
then A6: ( ON,W are_equipotent or ON in W ) by A1, CLASSES1:def 2;

now

let A be Ordinal; :: thesis: ( A,ON are_equipotent implies ON c= A )
assume that
A7: A,ON are_equipotent and
A8: not ON c= A ; :: thesis: contradiction
A in ON by A8, ORDINAL1:26;
then A in W by ORDINAL1:def 10;
hence contradiction by A1, A6, A5, A7, Th1, WELLORD2:22; :: thesis: verum

end;

then reconsider ON = ON as Cardinal by CARD_1:def 1;
ON = card ON by CARD_1:def 5;
hence On W = card W by A6, A5, CARD_1:21; :: thesis: verum