for n being non zero Nat holds n = {0} \/ ((Seg n) \ {n})