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