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

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

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

per cases ( 0 = r1 or 0 < r1 ) by A5, XXREAL_1:3;

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

( r2 < PI / 2 & PI / 2 < 2 * PI ) by A8, Lm1, XREAL_1:68, XXREAL_1:4;
then r2 < 2 * PI by XXREAL_0:2;
then cos r2 < 1 by A3, A10, SIN_COS6:34;
then A11: cos . r2 < 1 by SIN_COS:def 19;
( (- (PI / 2)) + ((2 * PI) * 0) < r2 & r2 < (PI / 2) + ((2 * PI) * 0) ) by A8, Lm1, XXREAL_1:4;
then cos r2 > 0 by SIN_COS6:13;
then cos . r2 > 0 by SIN_COS:def 19;
then A12: 1 / 1 < 1 / (cos . r2) by A11, XREAL_1:76;
sec . r1 = 1 / 1 by A4, A10, RFUNCT_1:def 2, SIN_COS:30
.= 1 ;
hence sec . r2 > sec . r1 by A7, A12, RFUNCT_1:def 2; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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