theorem Th23: :: INTEGRA7:23

sin is_integral_of cos , REAL