let i, j be natural Number ; :: thesis: ( i < j implies ex k being positive Nat st j = i + k )
assume A1: i < j ; :: thesis: ex k being positive Nat st j = i + k
then consider k being Nat such that
A2: j = i + k by NAT_1:10;

now :: thesis: not k <= 0

assume k <= 0 ; :: thesis: contradiction
then k = 0 ;
hence contradiction by A1, A2; :: thesis: verum

end;

then reconsider k = k as positive Nat ;
take k ; :: thesis: j = i + k
thus j = i + k by A2; :: thesis: verum