theorem Th1: :: AFINSQ_1:2

for n being Nat holds (Segm n) \/ {n} = Segm (n + 1)