theorem Th2: :: FLANG_2:2

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