theorem :: SIN_COS5:4

for x1, x2, x3 being Real st sin x1 <> 0 & sin x2 <> 0 & sin x3 <> 0 holds
cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3))))