:: deftheorem defines OddNAT NUMERAL2:def 2 :
OddNAT = { n where n is Nat : n is odd } ;