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