let A be Ordinal; :: thesis: for n being natural number st A,n are_equipotent holds
A = n
let n be natural number ; :: thesis: ( A,n are_equipotent implies A = n )
defpred S₁[ natural number ] means for A being Ordinal st A,$1 are_equipotent holds
A = $1;
A1: S₁[ {} ] by Th46;
A2: for n being natural number st S₁[n] holds
S₁[ succ n]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[ succ n] )
assume A3: S₁[n] ; :: thesis: S₁[ succ n]
let A be Ordinal; :: thesis: ( A, succ n are_equipotent implies A = succ n )
assume A4: A, succ n are_equipotent ; :: thesis: A = succ n
then A <> {} by Th46;
then A5: {} in A by ORDINAL3:10;

now

assume A is limit_ordinal ; :: thesis: contradiction
then A6: omega c= A by A5, ORDINAL1:def 12;
( card omega c= card A & card A = card (succ n) & card (succ n) in card omega ) by A4, A6, Lm1, Th21, Th27, Th83;
hence contradiction by ORDINAL1:7; :: thesis: verum

end;

then consider B being Ordinal such that
A7: A = succ B by ORDINAL1:42;
( B in A & n in succ n ) by A7, ORDINAL1:10;
then ( A \ {B},(succ n) \ {n} are_equipotent & A \ {B} = B & (succ n) \ {n} = n ) by A4, A7, Th61, ORDINAL1:52;
hence A = succ n by A3, A7; :: thesis: verum

end;

S₁[n] from ORDINAL2:sch 17(A1, A2);
hence ( A,n are_equipotent implies A = n ) ; :: thesis: verum