theorem Th9: :: INTEGRA8:9

[.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[