:: deftheorem defines CullenNumber NAT_6:def 6 :
for n being natural number holds CullenNumber n = (n * (2 |^ n)) + 1;