:: deftheorem defines sech SIN_COS5:def 2 :
for x being Real holds sech x = 1 / (cosh x);