:: deftheorem defines sec SIN_COS4:def 4 :
for th being Real holds sec th = 1 / (cos th);