theorem :: SIN_COS8:9

for x being Real holds ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x))