:: deftheorem defines POWEROF2SET ASYMPT_1:def 6 :
POWEROF2SET = { (2 to_power n) where n is Element of NAT : verum } ;