:: deftheorem defines EvenNAT FIB_NUM2:def 3 :
EvenNAT = { (2 * k) where k is Nat : verum } ;