now

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 ].0 ,(PI / 2).] & r1 in dom cosec & r2 in ].0 ,(PI / 2).] & r2 in dom cosec ) by A1, A2, XBOOLE_0:def 4;
then A5: ( 0 < r1 & r1 <= PI / 2 & 0 < r2 & r2 <= PI / 2 ) by XXREAL_1:2;

now

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

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

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

end;

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

A9: cosec . r2 = 1 / 1 by A4, A8, RFUNCT_1:def 8, SIN_COS:81
.= 1 ;
A10: sin . r1 > 0 by A4, Lm4, COMPTRIG:23;
sin r1 < 1 by A3, A5, A8, SIN_COS6:30;
then sin . r1 < 1 by SIN_COS:def 21;
then 1 / 1 < 1 / (sin . r1) by A10, XREAL_1:78;
hence cosec . r2 < cosec . r1 by A4, A9, RFUNCT_1:def 8; :: thesis: verum

end;

end;

end;

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

end;

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