theorem :: SIN_COS:55

for th being Real holds exp_R th > 0 by Th53;