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