theorem :: NAT_1:3

for i being natural Number st 0 <> i holds
0 < i by Th2;