theorem :: SIN_COS4:22

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