theorem :: SIN_COS5:3

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