theorem :: PRE_FF:7

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