theorem Th12: :: INTEGRA8:12

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