theorem :: AFINSQ_1:4

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