for m, n, k being Nat holds
( k in nat_interval (m,n) iff ( m <= k & k <= n ) )