theorem Th86: :: SINCOS10:86

for x being set st x in [.(- (sqrt 2)),(- 1).] holds
arcsec2 . x in [.((3 / 4) * PI),PI.]