let n be even Integer; :: thesis: n / 2 is Integer
consider j being Integer such that
A1: n = 2 * j by ABIAN:11;
thus n / 2 is Integer by A1; :: thesis: verum