let x be Real; :: thesis: ( sin (x / 2) <> 0 implies tan (x / 2) = (1 - (cos x)) / (sin x) )
assume sin (x / 2) <> 0 ; :: thesis: tan (x / 2) = (1 - (cos x)) / (sin x)
then A1: 2 * (sin (x / 2)) <> 0 ;
(1 - (cos x)) / (sin x) = (1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (sin (2 * (x / 2))) by Th7
.= ((2 * (sin (x / 2))) * (sin (x / 2))) / ((2 * (sin (x / 2))) * (cos (x / 2))) by Th5
.= tan (x / 2) by A1, XCMPLX_1:91 ;
hence tan (x / 2) = (1 - (cos x)) / (sin x) ; :: thesis: verum