for k, m, i being Nat st m <= i & i <= m + k holds
not not i = m + 0 & ... & not i = m + k