theorem Th9: :: FINSEQ_1:9

for a being natural Number holds (Seg a) \/ {(a + 1)} = Seg (a + 1)