let x be set ; :: thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arcsec2 . x in [.((3 / 4) * PI),PI.] )
A1: - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
assume x in [.(- (sqrt 2)),(- 1).] ; :: thesis: arcsec2 . x in [.((3 / 4) * PI),PI.]
then x in ].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} by A1, XXREAL_1:128;
then A2: ( 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 A2, TARSKI:def 2;

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

then A4: ( ].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).] & ex s being Real st
( s = x & - (sqrt 2) < s & s < - 1 ) ) by XXREAL_1:25;
A5: [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2) = [.(- (sqrt 2)),(- 1).] by Th46, XBOOLE_1:28;
then - 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2) by A1;
then A6: arcsec2 . x < PI by A3, A5, A4, Th74, Th82, RFUNCT_2:20;
- (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A1;
then (3 / 4) * PI < arcsec2 . x by A3, A5, A4, Th74, Th82, RFUNCT_2:20;
hence arcsec2 . x in [.((3 / 4) * PI),PI.] by A6; :: thesis: verum

end;

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

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

end;

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

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

end;

end;