theorem :: SIN_COS4:26

for th1, th2 being Real holds (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))