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