for i being Integer st i is Element of NAT holds
i div 2 is Element of NAT