let x be set ; :: thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] )
assume A1: x in [.(- (sqrt 2)),(- 1).] ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
A2: - (sqrt 2) < - 1 by SQUARE_1:84, XREAL_1:26;
then x in ].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} by A1, XXREAL_1:128;
then A3: ( x in ].(- (sqrt 2)),(- 1).[ or x in {(- (sqrt 2)),(- 1)} ) by XBOOLE_0:def 3;

per cases ( x in ].(- (sqrt 2)),(- 1).[ or x = - (sqrt 2) or x = - 1 ) by A3, TARSKI:def 2;

suppose A4: x in ].(- (sqrt 2)),(- 1).[ ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]

A5: - (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A2;
A6: [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1 ) = [.(- (sqrt 2)),(- 1).] by Th47, XBOOLE_1:28;
A7: ].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).] by XXREAL_1:25;
x in { s where s is Real : ( - (sqrt 2) < s & s < - 1 ) } by A4;
then A8: ex s being Real st
( s = x & - (sqrt 2) < s & s < - 1 ) ;
then A9: - (PI / 4) > arccosec1 . x by A4, A5, A6, A7, Th75, Th83, RFUNCT_2:44;
- 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1 ) by A2, A6;
then arccosec1 . x > - (PI / 2) by A4, A6, A7, A8, Th75, Th83, RFUNCT_2:44;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A9; :: thesis: verum

end;

suppose A10: x = - (sqrt 2) ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]

- (PI / 2) <= - (PI / 4) by Lm11, XXREAL_1:3;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A10, Th75; :: thesis: verum

end;

suppose A11: x = - 1 ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]

- (PI / 2) <= - (PI / 4) by Lm11, XXREAL_1:3;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A11, Th75; :: thesis: verum

end;

end;