theorem Th25: :: INTEGRA7:25

(- 1) (#) cos is_integral_of sin , REAL