let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) )
assume ( - (sqrt 2) <= r & r <= - 1 ) ; :: thesis: ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) )
then A1: r in [.(- (sqrt 2)),(- 1).] ;
then r in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) by Th47, RELAT_1:62;
then (arccosec1 | [.(- (sqrt 2)),(- 1).]) . r in rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) by FUNCT_1:def 3;
then arccosec1 r in rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) by A1, FUNCT_1:49;
hence ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) by Th99, XXREAL_1:1; :: thesis: verum