for m, k, n being Nat holds
( ( m + 1 <= k & k <= n ) iff ex i being Nat st
( m <= i & i < n & k = i + 1 ) )