theorem :: SIN_COS8:30

for x being Real st x < 0 holds
tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1)))