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