theorem Th6: :: INTEGRA8:6

for x being Real st sin (x / 2) < 0 holds
sin (x / 2) = - (sqrt ((1 - (cos x)) / 2))