theorem :: SGRAPH1:3

for n being Nat holds nat_interval (1,n) = Seg n ;