theorem :: SIN_COS4:43

for th1, th2 being Real st cos th1 <> 0 & cos th2 <> 0 holds
(sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))