theorem Th2: :: NAT_1:2

for i being natural Number holds 0 <= i