theorem Th29: :: INTEGRA8:29
(- cos) `| REAL = sin by Th26, FDIFF_1:def 7, SIN_COS:24;