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