let n, m be natural number ; :: thesis: ( n,m are_equipotent implies n = m )
defpred S₁[ natural number ] means for n being natural number st n,$1 are_equipotent holds
n = $1;
A1: for a being natural number st S₁[a] holds
S₁[ succ a]

proof

let a be natural number ; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume A2: S₁[a] ; :: thesis: S₁[ succ a]
let n be natural number ; :: thesis: ( n, succ a are_equipotent implies n = succ a )
assume A3: n, succ a are_equipotent ; :: thesis: n = succ a

per cases ( n = {} or n <> {} ) ;

suppose n = {} ; :: thesis: n = succ a

hence n = succ a by A3, Th46; :: thesis: verum

end;

suppose n <> {} ; :: thesis: n = succ a

then ex m being natural number st n = succ m by Th63;
hence n = succ a by A2, A3, Th62; :: thesis: verum

end;

end;

end;

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