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