now

let r1, r2 be Real; :: thesis: ( r1 in ].(PI / 2),PI .] /\ (dom sec ) & r2 in ].(PI / 2),PI .] /\ (dom sec ) & r1 < r2 implies sec . r2 > sec . r1 )
assume that
A1: r1 in ].(PI / 2),PI .] /\ (dom sec ) and
A2: r2 in ].(PI / 2),PI .] /\ (dom sec ) and
A3: r1 < r2 ; :: thesis: sec . r2 > sec . r1
A4: ( r1 in ].(PI / 2),PI .] & r1 in dom sec & r2 in ].(PI / 2),PI .] & r2 in dom sec ) by A1, A2, XBOOLE_0:def 4;
then A5: ( PI / 2 < r1 & r1 <= PI & PI / 2 < r2 & r2 <= PI ) by XXREAL_1:2;

now

per cases ( r2 < PI or r2 = PI ) by A5, XXREAL_0:1;

suppose A6: r2 < PI ; :: thesis: sec . r2 > sec . r1

then r1 < PI by A3, XXREAL_0:2;
then r1 in ].(PI / 2),PI .[ by A5, XXREAL_1:4;
then A7: r1 in ].(PI / 2),PI .[ /\ (dom sec ) by A4, XBOOLE_0:def 4;
r2 in ].(PI / 2),PI .[ by A5, A6, XXREAL_1:4;
then r2 in ].(PI / 2),PI .[ /\ (dom sec ) by A4, XBOOLE_0:def 4;
hence sec . r2 > sec . r1 by A3, A7, Th14, RFUNCT_2:43; :: thesis: verum

end;

suppose A8: r2 = PI ; :: thesis: sec . r1 < sec . r2

A9: sec . r2 = 1 / (- 1) by A4, A8, RFUNCT_1:def 8, SIN_COS:81
.= - 1 ;
PI * 1 < PI * (3 / 2) by XREAL_1:70;
then ( (PI / 2) + ((2 * PI ) * 0 ) < r1 & r1 < ((3 / 2) * PI ) + ((2 * PI ) * 0 ) ) by A3, A4, A8, XXREAL_0:2, XXREAL_1:2;
then cos r1 < 0 by SIN_COS6:14;
then A11: cos . r1 < 0 by SIN_COS:def 23;
( r1 > 0 & r1 < PI ) by A3, A5, XXREAL_0:2;
then cos r1 > - 1 by SIN_COS6:35;
then cos . r1 > - 1 by SIN_COS:def 23;
then (cos . r1) " < (- 1) " by A11, XREAL_1:89;
hence sec . r1 < sec . r2 by A4, A9, RFUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence sec . r2 > sec . r1 ; :: thesis: verum

end;

hence sec | ].(PI / 2),PI .] is increasing by RFUNCT_2:43; :: thesis: verum