let x be set ; :: thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arcsec2 . x in [.((3 / 4) * PI ),PI .] )
assume A1: x in [.(- (sqrt 2)),(- 1).] ; :: thesis: arcsec2 . x in [.((3 / 4) * PI ),PI .]
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: arcsec2 . x in [.((3 / 4) * PI ),PI .]

A5: - (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A2;
A6: [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2 ) = [.(- (sqrt 2)),(- 1).] by Th46, 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: (3 / 4) * PI < arcsec2 . x by A4, A5, A6, A7, Th74, Th82, RFUNCT_2:43;
- 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2 ) by A2, A6;
then arcsec2 . x < PI by A4, A6, A7, A8, Th74, Th82, RFUNCT_2:43;
hence arcsec2 . x in [.((3 / 4) * PI ),PI .] by A9; :: thesis: verum

end;

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

(3 / 4) * PI <= PI by Lm10, XXREAL_1:2;
hence arcsec2 . x in [.((3 / 4) * PI ),PI .] by A10, Th74; :: thesis: verum

end;

suppose A11: x = - 1 ; :: thesis: arcsec2 . x in [.((3 / 4) * PI ),PI .]

(3 / 4) * PI <= PI by Lm10, XXREAL_1:2;
hence arcsec2 . x in [.((3 / 4) * PI ),PI .] by A11, Th74; :: thesis: verum

end;

end;