theorem Th3: :: INT_1:3

for i0 being Integer st 0 <= i0 holds
i0 in NAT