theorem Th20: :: MIDSP_3:20

for n being Nat holds 1 in Seg (n + 1)