now :: thesis: for r1, r2 being Real st r1 in ].(PI / 2),PI.] /\ (dom sec) & r2 in ].(PI / 2),PI.] /\ (dom sec) & r1 < r2 holds
sec . r2 > sec . r1

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 dom sec by A1, XBOOLE_0:def 4;
A5: r2 in dom sec by A2, XBOOLE_0:def 4;
A6: r1 in ].(PI / 2),PI.] by A1, XBOOLE_0:def 4;
then A7: PI / 2 < r1 by XXREAL_1:2;
A8: r2 in ].(PI / 2),PI.] by A2, XBOOLE_0:def 4;
then A9: r2 <= PI by XXREAL_1:2;
A10: PI / 2 < r2 by A8, XXREAL_1:2;

now :: thesis: sec . r2 > sec . r1

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

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

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

end;

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

PI * 1 < PI * (3 / 2) by XREAL_1:68;
then A14: r1 < ((3 / 2) * PI) + ((2 * PI) * 0) by A3, A13, XXREAL_0:2;
(PI / 2) + ((2 * PI) * 0) < r1 by A6, XXREAL_1:2;
then cos r1 < 0 by A14, SIN_COS6:14;
then A15: cos . r1 < 0 by SIN_COS:def 19;
r1 < PI by A3, A9, XXREAL_0:2;
then cos r1 > - 1 by A7, SIN_COS6:35;
then cos . r1 > - 1 by SIN_COS:def 19;
then A16: (cos . r1) " < (- 1) " by A15, XREAL_1:87;
sec . r2 = 1 / (- 1) by A5, A13, RFUNCT_1:def 2, SIN_COS:76
.= - 1 ;
hence sec . r1 < sec . r2 by A4, A16, RFUNCT_1:def 2; :: thesis: verum

end;

end;

end;

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

end;

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