let th1, th2 be Real; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2)) )
assume ( cos th1 <> 0 & cos th2 <> 0 ) ; :: thesis: (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2))
then (tan th1) - (tan th2) = (((sin th1) * (cos th2)) - ((sin th2) * (cos th1))) / ((cos th1) * (cos th2)) by XCMPLX_1:130
.= (sin (th1 - th2)) / ((cos th1) * (cos th2)) by SIN_COS:82 ;
hence (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2)) ; :: thesis: verum