theorem :: SIN_COS5:35

for x being Real st sin (x / 2) <> 0 & cos (x / 2) <> 0 & 1 - ((tan (x / 2)) ^2) <> 0 & not cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) holds
cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1)))