theorem :: SIN_COS4:10

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