let k, m, i be Nat; :: thesis: ( m <= i & i <= m + k implies not not i = m + 0 & ... & not i = m + k )
assume that
A1: m <= i and
A2: i <= m + k ; :: thesis: not not i = m + 0 & ... & not i = m + k
take j = i; :: thesis: ( m + 0 <= j & j <= m + k & i = j )
thus ( m + 0 <= j & j <= m + k & i = j ) by A1, A2; :: thesis: verum