theorem :: SIN_COS5:28

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