theorem :: SIN_COS5:30

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