theorem :: SIN_COS5:27

for x being Real holds
( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )