theorem :: SIN_COS4:34

for th1, th2, th3 being Real holds ((sin th1) * (sin th2)) * (cos th3) = (1 / 4) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3)))