theorem Th24: :: SIN_COS8:24

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