theorem :: SIN_COS8:29

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