theorem Th5: :: INTEGRA8:5

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