2 divides a by ABIAN:def 1;
then consider k being Integer such that
A1: a = 2 * k ;
thus a / 2 is integer by A1; :: thesis: verum