:: deftheorem defines nat_interval SGRAPH1:def 1 :
for m, n being Nat holds nat_interval (m,n) = { i where i is Nat : ( m <= i & i <= n ) } ;