theorem Th4: :: SGRAPH1:4

for m, n being Nat st 1 <= m holds
nat_interval (m,n) c= Seg n