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