now

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

now

per cases ( 0 = r1 or 0 < r1 ) by A5;

suppose A6: 0 = r1 ; :: thesis: sec . r2 > sec . r1

A8: sec . r1 = 1 / 1 by A4, A6, RFUNCT_1:def 8, SIN_COS:33
.= 1 ;
A9: ( - (PI / 2) < r2 & r2 < PI / 2 ) by A4, Lm1, XXREAL_1:4;
( (- (PI / 2)) + ((2 * PI ) * 0 ) < r2 & r2 < (PI / 2) + ((2 * PI ) * 0 ) ) by A4, Lm1, XXREAL_1:4;
then cos r2 > 0 by SIN_COS6:13;
then A10: cos . r2 > 0 by SIN_COS:def 23;
PI / 2 < 2 * PI by XREAL_1:70;
then r2 < 2 * PI by A9, XXREAL_0:2;
then cos r2 < 1 by A3, A6, SIN_COS6:34;
then cos . r2 < 1 by SIN_COS:def 23;
then 1 / 1 < 1 / (cos . r2) by A10, XREAL_1:78;
hence sec . r2 > sec . r1 by A4, A8, RFUNCT_1:def 8; :: thesis: verum

end;

suppose A13: 0 < r1 ; :: thesis: sec . r2 > sec . r1

then r1 in ].0 ,(PI / 2).[ by A5;
then A14: r1 in ].0 ,(PI / 2).[ /\ (dom sec ) by A4, XBOOLE_0:def 4;
0 < r2 by A3, A13;
then r2 in ].0 ,(PI / 2).[ by A5;
then r2 in ].0 ,(PI / 2).[ /\ (dom sec ) by A4, XBOOLE_0:def 4;
hence sec . r2 > sec . r1 by A3, A14, Th13, RFUNCT_2:43; :: thesis: verum

end;

end;

end;

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

end;

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