:: deftheorem defines OddNAT FIB_NUM2:def 4 :
OddNAT = { ((2 * k) + 1) where k is Element of NAT : verum } ;