2 divides j by ABIAN:def 1;
then consider l being Integer such that
A1: j = 2 * l by INT_1:def 9;
2 divides i by ABIAN:def 1;
then consider k being Integer such that
A2: i = 2 * k by INT_1:def 9;
i - j = 2 * (k - l) by A2, A1;
hence i - j is even ; :: thesis: verum