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