theorem :: SIN_COS4:14

for th1, th2, th3 being Real st sin th1 <> 0 & sin th2 <> 0 & sin th3 <> 0 holds
cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1)