let i, j be odd Nat; :: thesis: ( i <= j implies ex k being natural number st i + (2 * k) = j )
assume i <= j ; :: thesis: ex k being natural number st i + (2 * k) = j
then consider jjj being Nat such that
A1: j = i + jjj by NAT_1:10;
A2: jjj in NAT by ORDINAL1:def 13;
jjj is even by A1;
then consider jj being Element of NAT such that
A3: 2 * jj = jjj by A2, ABIAN:def 2;
reconsider jj = jj as Nat ;
take jj ; :: thesis: i + (2 * jj) = j
thus i + (2 * jj) = j by A1, A3; :: thesis: verum