theorem :: SIN_COS4:44

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