:: deftheorem defines number_e IRRAT_1:def 7 :
number_e = exp_R 1;