:: deftheorem defines double_odd NUMBER04:def 2 :
for i being Nat holds
( i is double_odd iff ex j being odd Nat st i = 2 * j );