theorem :: SIN_COS4:28

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