theorem Th1: :: FLANG_2:1

for i, k, m, n being Nat st m + k <= i & i <= n + k holds
ex mn being Nat st
( mn + k = i & m <= mn & mn <= n )