theorem Th28: :: INTEGRA8:28

cos `| REAL = - sin