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