theorem :: SIN_COS5:29

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