theorem Th2: :: SIN_COS8:2
for x being Real holds
( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) )