let i0, i1 be Integer; :: thesis: ( i0 <= i1 implies ex k being Nat st i0 + k = i1 )
assume i0 <= i1 ; :: thesis: ex k being Nat st i0 + k = i1
then reconsider k = i1 - i0 as Element of NAT by Th5;
i0 + k = i1 ;
hence ex k being Nat st i0 + k = i1 ; :: thesis: verum