theorem Th8: :: FINSEQ_3:8

for k being Nat holds not k + 1 in Seg k