theorem :: SIN_COS4:24

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