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