let i, j be odd Nat; :: thesis: ( i <= j implies ex k being Nat st i + (2 * k) = j )
assume i <= j ; :: thesis: ex k being Nat st i + (2 * k) = j
then consider jjj being Nat such that
A1: j = i + jjj by NAT_1:10;
jjj is even by A1;
then consider jj being Nat such that
A2: 2 * jj = jjj by ABIAN:def 2;
take jj ; :: thesis: i + (2 * jj) = j
thus i + (2 * jj) = j by A1, A2; :: thesis: verum