theorem Th4: :: BINARI_4:4

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