for k, m, n being Nat st k < m holds
Seg k misses nat_interval (m,n)