:: deftheorem defines EvenNAT NUMERAL2:def 1 :
EvenNAT = { n where n is Nat : n is even } ;