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