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 ;
(i / 2) - 1 < [\(i / 2)/] by INT_1:def 6;
then A1: i / 2 < [\(i / 2)/] + 1 by XREAL_1:19;
n >= 0 ;
then i / 2 >= 0 / 2 ;
then [\(i / 2)/] is Element of NAT by A1, INT_1:3, INT_1:7;
hence i div 2 is Element of NAT by INT_1:def 9; :: thesis: verum