ex j being Integer st i = 2 * j by Lm1;
hence not i + 1 is even by Th1; :: thesis: verum