for n being Nat holds Seg n = (n + 1) \ {0}