theorem :: SIN_COS5:48

for x being Real holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)