let x be Real; :: thesis: ( sin (x / 2) < 0 implies sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
assume A1: sin (x / 2) < 0 ; :: thesis: sin (x / 2) = - (sqrt ((1 - (cos x)) / 2))
sqrt ((1 - (cos x)) / 2) = sqrt ((1 - (cos (2 * (x / 2)))) / 2)
.= sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2) by SIN_COS5:7
.= |.(sin (x / 2)).| by COMPLEX1:72
.= - (sin (x / 2)) by A1, ABSVALUE:def 1 ;
hence sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) ; :: thesis: verum