theorem Th5: :: RADIX_2:5

for i, n being Nat st i in Seg n holds
i + 1 in Seg (n + 1)