theorem Th87: :: SINCOS10:87

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