let m, n be Nat; :: thesis: ( n,m are_equipotent implies n = m )
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]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume A2: S₁[a] ; :: thesis: S₁[ succ a]
let n be Nat; :: 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, RELAT_1:42; :: thesis: verum

end;

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

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

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: verum