theorem Th8: :: BINARI_4:8

for k, l, m being Nat st l + m <= k - 1 holds
( l < k & m < k )