theorem :: SIN_COS7:64

for x, y being Real st y = (1 / 2) * ((exp_R x) + (exp_R (- x))) & 1 <= y & not x = log (number_e,(y + (sqrt ((y ^2) - 1)))) holds
x = - (log (number_e,(y + (sqrt ((y ^2) - 1)))))