theorem Th25: :: SIN_COS8:25

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