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

per cases ( x in ].(- (PI / 2)),(- (PI / 4)).[ or x = - (PI / 2) or x = - (PI / 4) ) by A2, TARSKI:def 2;

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

then A4: ex s being Real st
( s = x & - (PI / 2) < s & s < - (PI / 4) ) ;
A5: ex s being Real st
( s = x & - (PI / 2) < s & s < - (PI / 4) ) by A3;
A6: ].(- (PI / 2)),(- (PI / 4)).[ c= [.(- (PI / 2)),(- (PI / 4)).] by XXREAL_1:25;
( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) by A1;
then A7: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by XXREAL_2:def 12;
then A8: cosec | [.(- (PI / 2)),(- (PI / 4)).] is decreasing by Th19, RFUNCT_2:29;
A9: [.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec) = [.(- (PI / 2)),(- (PI / 4)).] by A7, Th3, XBOOLE_1:1, XBOOLE_1:28;
then - (PI / 4) in [.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec) by A1;
then A10: cosec . x > - (sqrt 2) by A3, A8, A9, A6, A5, Th32, RFUNCT_2:21;
- (PI / 2) in [.(- (PI / 2)),(- (PI / 4)).] by A1;
then - 1 > cosec . x by A3, A8, A9, A6, A4, Th32, RFUNCT_2:21;
hence cosec . x in [.(- (sqrt 2)),(- 1).] by A10; :: thesis: verum

end;

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

- (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
hence cosec . x in [.(- (sqrt 2)),(- 1).] by A11, Th32; :: thesis: verum

end;

suppose A12: x = - (PI / 4) ; :: thesis: cosec . x in [.(- (sqrt 2)),(- 1).]

- (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
hence cosec . x in [.(- (sqrt 2)),(- 1).] by A12, Th32; :: thesis: verum

end;

end;