theorem :: DESCIP_1:19

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