theorem Th2: :: AFINSQ_1:3

for n being Nat holds Seg n c= Segm (n + 1)