theorem Th27: :: INTEGRA8:27

sin `| REAL = cos