:: deftheorem defines cosh2" SIN_COS7:def 3 :
for x being Real holds cosh2" x = - (log (number_e,(x + (sqrt ((x ^2) - 1)))));