for n, m, k being Nat st k < m holds
n + k in n + m