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

let a be Nat; :: thesis:
assume A2: S₁[a] ; :: thesis:
let n be Nat; :: thesis:
assume A3: n, succ a are_equipotent ; :: thesis:

suppose n = {} ; :: thesis:

hence n = succ a by A3, RELAT_1:42; :: thesis:

end;

suppose n <> {} ; :: thesis:

then ex m being Nat st n = succ m by Th35;
hence n = succ a by A2, A3, Th34; :: thesis:

end;

end;

end;

A4: S₁[ 0 ] by Th25;
S₁[m] from ORDINAL2:sch 17(A4, A1);
hence ( n,m are_equipotent implies n = m ) ; :: thesis: