let x be set ; ( 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).]
; 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).[
;
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;
verum end; end;