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