let th1, th2 be Real; :: thesis: ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2))
((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / ((sin th1) - (sin th2)) by Th15
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) by Th16
.= (2 / 2) * (((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) / ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) by XCMPLX_1:76
.= (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2)) by XCMPLX_1:76 ;
hence ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2)) ; :: thesis: verum