theorem Th5: :: SGRAPH1:5

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