theorem Th28: :: INTEGRA8:28
cos `| REAL = - sin