let A be Ordinal; :: thesis: for n being Nat st A,n are_equipotent holds
A = n
let n be Nat; :: thesis: ( A,n are_equipotent implies A = n )
defpred S1[ Nat] means for A being Ordinal st A,$1 are_equipotent holds
A = $1;
A1: for n being Nat st S1[n] holds
S1[ succ n]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[ succ n] )
assume A2: S1[n] ; :: thesis: S1[ 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 RELAT_1:42;
then A5: {} in A by ORDINAL3:8;
now :: thesis: not A is limit_ordinal
A6: succ n in omega by ORDINAL1:def 12;
assume A is limit_ordinal ; :: thesis: contradiction
then A7: omega c= A by A5, ORDINAL1:def 11;
card A = card (succ n) by A4, Th4;
hence contradiction by A7, Lm1, Th10, ORDINAL1:5, A6; :: thesis: verum
end;
then consider B being Ordinal such that
A8: A = succ B by ORDINAL1:29;
( B in A & A \ {B} = B ) by A8, ORDINAL1:6, ORDINAL1:37;
hence A = succ n by A2, A4, A8, A3, Th33; :: thesis: verum
end;
A9: S1[ 0 ] by Th25;
S1[n] from ORDINAL2:sch 17(A9, A1);
hence ( A,n are_equipotent implies A = n ) ; :: thesis: verum