let n be Nat; :: thesis: ( n is odd iff ex k being Nat st n = (2 * k) + 1 )

hereby :: thesis: ( ex k being Nat st n = (2 * k) + 1 implies n is odd )

assume A1: n is odd ; :: thesis: ex j being Nat st n = (2 * j) + 1
then consider j being Integer such that
A2: n = (2 * j) + 1 by Th1;

now :: thesis: not j < 0

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; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

thus ( ex k being Nat st n = (2 * k) + 1 implies n is odd ) ; :: thesis: verum