theorem Th8: :: MIDSP_3:8

for n, i being Nat st i <= n holds
i + 1 is Nat of n