consider k being Integer such that
A1: i = (2 * k) + 1 by Th1;
consider l being Integer such that
A2: j = (2 * l) + 1 by Th1;
i - j = 2 * (k - l) by A1, A2;
hence i - j is even ; :: thesis: verum