theorem Th5: :: BAGORD_2:3

for m, n, x, y being Nat st n = (m -' x) + y holds
( m -' n <= x & n -' m <= y )