thus ( i is double_odd implies ex j being odd Nat st i = 2 * j ) :: thesis: ( ex j being odd Nat st i = 2 * j implies i is double_odd )

proof

given j being odd Integer such that A1: i = 2 * j ; :: according to NUMBER04:def 1 :: thesis: ex j being odd Nat st i = 2 * j
j >= 0 by A1;
then reconsider j = j as odd Element of NAT by INT_1:3;
take j ; :: thesis: i = 2 * j
thus i = 2 * j by A1; :: thesis: verum

end;

thus ( ex j being odd Nat st i = 2 * j implies i is double_odd ) ; :: thesis: verum