let i be Integer; :: thesis: ( i is Element of NAT implies i div 2 is Element of NAT )
assume i is Element of NAT ; :: thesis: i div 2 is Element of NAT
then reconsider n = i as Element of NAT ;
n >= 0 ;
then i / 2 >= 0 / 2 ;
then [\(i / 2)/] is Element of NAT by INT_1:3;
hence i div 2 is Element of NAT by INT_1:def 9; :: thesis: verum