let n be even Integer; :: thesis: n / 2 is Integer
ex j being Integer st n = 2 * j by ABIAN:11;
hence n / 2 is Integer ; :: thesis: verum