theorem Th66: :: SIN_COS:67

for th being Real holds
( cos is_differentiable_on REAL & diff (cos,th) = - (sin . th) )