let W be set ; :: thesis: ( W is Tarski implies On W = card W )
assume A1: W is Tarski ; :: thesis: On W = card W
then A2: W is subset-closed ;

now

let X be set ; :: thesis: ( X in On W implies ( X is Ordinal & X c= On W ) )
assume A3: X in On W ; :: thesis: ( X is Ordinal & X c= On W )
then A4: ( X in W & X is Ordinal ) by ORDINAL1:def 10;
thus X is Ordinal by A3, ORDINAL1:def 10; :: thesis: X c= On W
reconsider A = X as Ordinal by A3, 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 A5: x in X ; :: thesis: x in On W
then x in A ;
then reconsider B = x as Ordinal ;
B c= A by A5, ORDINAL1:def 2;
then B in W by A2, A4, 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;
ON c= W by ORDINAL2:9;
then A6: ( ON,W are_equipotent or ON in W ) by A1, CLASSES1:def 2;

A7: now

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

end;

now

let A be Ordinal; :: thesis: ( A,ON are_equipotent implies ON c= A )
assume ( A,ON are_equipotent & not ON c= A ) ; :: thesis: contradiction
then A8: ( A,W are_equipotent & A in ON ) by A6, A7, ORDINAL1:26, WELLORD2:22;
then A in W by ORDINAL1:def 10;
hence contradiction by A2, A8, Th1; :: 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, A7, CARD_1:21; :: thesis: verum