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