let m, n be Nat; :: thesis: ( m < n implies ex k being Nat st
( m + k = n & k > 0 ) )
assume m < n ; :: thesis: ex k being Nat st
( m + k = n & k > 0 )
then ( ex k being Nat st m + k = n & m - m < n - m ) by NAT_1:10, XREAL_1:14;
hence ex k being Nat st
( m + k = n & k > 0 ) ; :: thesis: verum