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

now :: thesis: for X being set st X in On W holds
( X is Ordinal & X c= On W )

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 9; :: thesis: X c= On W
reconsider A = X as Ordinal by A2, ORDINAL1:def 9;
A3: X in W by A2, ORDINAL1:def 9;
thus X c= On W :: thesis: verum

proof

let x be object ; :: 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 9; :: thesis: verum

end;

end;

then reconsider ON = On W as epsilon-transitive epsilon-connected set by ORDINAL1:19;

A5: now :: thesis: not ON in W

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

end;

ON c= W by ORDINAL2:7;
then A6: ( ON,W are_equipotent or ON in W ) by A1;

now :: thesis: for A being Ordinal st A,ON are_equipotent holds
ON c= A

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:16;
then A in W by ORDINAL1:def 9;
hence contradiction by A1, A6, A5, A7, Th1, WELLORD2:15; :: thesis: verum

end;

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