consider k being Integer such that
A1: n = 2 * k by ABIAN:def 1, INT_1:def 3;
k >= 0 by A1;
then k in NAT by INT_1:3;
then reconsider k = k as natural number ;
n / 2 = k by A1;
hence n / 2 is natural ; :: thesis: verum