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