theorem :: SGRAPH1:1

for m, n being Nat
for e being set holds
( e in nat_interval (m,n) iff ex i being Nat st
( e = i & m <= i & i <= n ) ) ;