:: deftheorem defines cosech SIN_COS5:def 3 :
for x being Real holds cosech x = 1 / (sinh x);