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