theorem Th52: :: SIN_COS:53

for th being Real st th < 0 holds
( 0 < exp_R . th & exp_R . th <= 1 )