theorem :: NAT_1:5

for i being natural Number holds 0 < i + 1