theorem :: SIN_COS5:33

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