theorem Th3: :: HILB10_3:3

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