theorem Th7: :: MIDSP_3:7

for n, i being Nat holds
( i is Nat of n iff i in Seg (n + 1) )