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: 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 A2: S₁[n] ; :: thesis: S₁[ succ n]
let A be Ordinal; :: thesis: ( A, succ n are_equipotent implies A = succ n )
A3: ( n in succ n & (succ n) \ {n} = n ) by ORDINAL1:6, ORDINAL1:37;
assume A4: A, succ n are_equipotent ; :: thesis: A = succ n
then A <> {} by Th46;
then A5: {} in A by ORDINAL3:8;

now

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

end;

then consider B being Ordinal such that
A7: A = succ B by ORDINAL1:29;
( B in A & A \ {B} = B ) by A7, ORDINAL1:6, ORDINAL1:37;
hence A = succ n by A2, A4, A7, A3, Th61; :: thesis: verum

end;

A8: S₁[ {} ] by Th46;
S₁[n] from ORDINAL2:sch 17(A8, A1);
hence ( A,n are_equipotent implies A = n ) ; :: thesis: verum