:: deftheorem defines cosec SIN_COS4:def 3 :
for th being Real holds cosec th = 1 / (sin th);