:: deftheorem defines Oddity NEWTON05:def 4 :
for a being Integer holds Oddity a = a / (Parity a);