theorem :: SIN_COS4:46

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