theorem Th67: :: SIN_COS:68

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