theorem Th26: :: NAT_1:38

for n being Nat holds succ (Segm n) = Segm (n + 1)