theorem Th15: :: INTEGRA8:15
arccos ((sqrt 2) / 2) = PI / 4