theorem :: SIN_COS4:42

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