for i being natural Number holds
( i = 0 or ex k being Nat st i = k + 1 )