:: deftheorem defines cos SIN_COS:def 19 :
for th being Real holds cos th = cos . th;