theorem Th6: :: NAT_1:6

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