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