theorem :: SIN_COS5:34

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