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

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

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

(PI / 4) + (PI / 4) < (PI / 2) + (PI / 4) by A1, XREAL_1:10;
then A5: (3 / 4) * PI in ].(PI / 2),PI .] by A2;
PI in ].(PI / 2),PI .] by COMPTRIG:21;
then A6: [.((3 / 4) * PI ),PI .] c= ].(PI / 2),PI .] by A5, XXREAL_2:def 12;
then A7: sec | [.((3 / 4) * PI ),PI .] is increasing by Th18, RFUNCT_2:60;
A8: ex s being Real st
( s = x & (3 / 4) * PI < s & s < PI ) by A4;
A9: ex s being Real st
( s = x & (3 / 4) * PI < s & s < PI ) by A4;
A10: ].((3 / 4) * PI ),PI .[ c= [.((3 / 4) * PI ),PI .] by XXREAL_1:25;
A11: [.((3 / 4) * PI ),PI .] /\ (dom sec ) = [.((3 / 4) * PI ),PI .] by A6, Th2, XBOOLE_1:1, XBOOLE_1:28;
then PI in [.((3 / 4) * PI ),PI .] /\ (dom sec ) by A2;
then A12: sec . x < - 1 by A4, A7, A11, A10, A9, Th31, RFUNCT_2:43;
(3 / 4) * PI in [.((3 / 4) * PI ),PI .] by A2;
then - (sqrt 2) < sec . x by A4, A7, A11, A10, A8, Th31, RFUNCT_2:43;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A12; :: thesis: verum

end;

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

- (sqrt 2) < - 1 by SQUARE_1:84, XREAL_1:26;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A13, Th31; :: thesis: verum

end;

suppose A14: x = PI ; :: thesis: sec . x in [.(- (sqrt 2)),(- 1).]

- (sqrt 2) < - 1 by SQUARE_1:84, XREAL_1:26;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A14, Th31; :: thesis: verum

end;

end;