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