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

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

now :: thesis: cosec . r2 < cosec . r1

per cases ( r2 < PI / 2 or r2 = PI / 2 ) by A6, XXREAL_0:1;

suppose A11: r2 < PI / 2 ; :: thesis: cosec . r2 < cosec . r1

then r1 < PI / 2 by A3, XXREAL_0:2;
then r1 in ].0,(PI / 2).[ by A9;
then A12: r1 in ].0,(PI / 2).[ /\ (dom cosec) by A4, XBOOLE_0:def 4;
r2 in ].0,(PI / 2).[ by A10, A11;
then r2 in ].0,(PI / 2).[ /\ (dom cosec) by A7, XBOOLE_0:def 4;
hence cosec . r2 < cosec . r1 by A3, A12, Th16, RFUNCT_2:21; :: thesis: verum

end;

suppose A13: r2 = PI / 2 ; :: thesis: cosec . r2 < cosec . r1

then sin r1 < 1 by A3, A9, SIN_COS6:30;
then A14: sin . r1 < 1 by SIN_COS:def 17;
sin . r1 > 0 by A8, Lm4, COMPTRIG:7;
then A15: 1 / 1 < 1 / (sin . r1) by A14, XREAL_1:76;
cosec . r2 = 1 / 1 by A7, A13, RFUNCT_1:def 2, SIN_COS:76
.= 1 ;
hence cosec . r2 < cosec . r1 by A4, A15, RFUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence cosec . r2 < cosec . r1 ; :: thesis: verum

end;

hence cosec | ].0,(PI / 2).] is decreasing by RFUNCT_2:21; :: thesis: verum