let th1, th2 be Real; ( sin ((th1 - th2) / 2) <> 0 implies ((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2) )
assume A1:
sin ((th1 - th2) / 2) <> 0
; ((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2)
((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) =
(2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / ((cos th2) - (cos th1))
by Th16
.=
(2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (- (2 * ((sin ((th2 + th1) / 2)) * (sin ((th2 - th1) / 2)))))
by Th18
.=
(2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (- (sin ((th2 - th1) / 2)))))
.=
(2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (sin (- ((th2 - th1) / 2)))))
by SIN_COS:31
.=
(2 / 2) * (((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) / ((sin ((th2 + th1) / 2)) * (sin ((th1 - th2) / 2))))
by XCMPLX_1:76
.=
((cos ((th1 + th2) / 2)) / (sin ((th2 + th1) / 2))) * ((sin ((th1 - th2) / 2)) / (sin ((th1 - th2) / 2)))
by XCMPLX_1:76
.=
cot ((th1 + th2) / 2)
by A1, XCMPLX_1:88
;
hence
((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2)
; verum