theorem :: SGRAPH1:6

for m, n being Nat st n < m holds
nat_interval (m,n) = {}