ex k being Integer st n = 2 * k by ABIAN:def 1, INT_1:def 3;
hence n / 2 is integer ; :: thesis: verum