let th1, th2 be Real; :: thesis: (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))
(cos (th1 + th2)) - (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) - (cos (th1 - th2)) by SIN_COS:75
.= (((cos th1) * (cos th2)) + (- ((sin th1) * (sin th2)))) - (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) by SIN_COS:83
.= - (2 * ((sin th1) * (sin th2))) ;
hence (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2))) ; :: thesis: verum