let th1, th2 be Real; :: thesis: ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2))
((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / ((cos th1) - (cos th2)) by Th17
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (- (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))) by Th18
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (2 * ((sin ((th1 + th2) / 2)) * (- (sin ((th1 - th2) / 2)))))
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (2 * ((sin ((th1 + th2) / 2)) * (sin (- ((th1 - th2) / 2))))) by SIN_COS:31
.= (2 / 2) * (((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) / ((sin ((th1 + th2) / 2)) * (sin ((th2 - th1) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 + th2) / 2)) / (sin ((th1 + th2) / 2))) * ((cos (- ((th2 - th1) / 2))) / (sin ((th2 - th1) / 2))) by XCMPLX_1:76
.= (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2)) by SIN_COS:31 ;
hence ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2)) ; :: thesis: verum