let n be natural number ; :: thesis: ( not n is even iff ex k being Element of NAT st n = (2 * k) + 1 )

hereby :: thesis: ( ex k being Element of NAT st n = (2 * k) + 1 implies not n is even )

assume A1: not n is even ; :: thesis: ex j being Element of NAT st n = (2 * j) + 1
then consider j being Integer such that
A2: n = (2 * j) + 1 by Th1;

now

assume j < 0 ; :: thesis: contradiction
then A3: (2 * j) + 1 <= 2 * 0 by INT_1:7, XREAL_1:68;

per cases ( (2 * j) + 1 < 0 or (2 * j) + 1 = 0 ) by A3;

suppose (2 * j) + 1 < 0 ; :: thesis: contradiction

hence contradiction by A2, NAT_1:2; :: thesis: verum

end;

suppose (2 * j) + 1 = 0 ; :: thesis: contradiction

then n = 2 * 0 ;
hence contradiction by A1; :: thesis: verum

end;

end;

end;

then reconsider j = j as Element of NAT by INT_1:3;
take j = j; :: thesis: n = (2 * j) + 1
thus n = (2 * j) + 1 by A2; :: thesis: verum

end;

thus ( ex k being Element of NAT st n = (2 * k) + 1 implies not n is even ) ; :: thesis: verum