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

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

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

per cases ( - (PI / 2) = r1 or - (PI / 2) < r1 ) by A10, XXREAL_0:1;

suppose A11: - (PI / 2) = r1 ; :: thesis: cosec . r2 < cosec . r1

- (PI / 2) > - PI by COMPTRIG:5, XREAL_1:24;
then A12: ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by XXREAL_1:46;
r2 in ].(- (PI / 2)),0.[ by A3, A9, A11;
then - PI < r2 by A12, XXREAL_1:4;
then A13: (- PI) + (2 * PI) < r2 + (2 * PI) by XREAL_1:8;
r2 + (2 * PI) < 0 + (2 * PI) by A9, XREAL_1:8;
then r2 + (2 * PI) in ].PI,(2 * PI).[ by A13;
then sin . (r2 + (2 * PI)) < 0 by COMPTRIG:9;
then A14: sin . r2 < 0 by SIN_COS:78;
A15: r2 < (2 * PI) + ((2 * PI) * (- 1)) by A8, XXREAL_1:3;
((3 / 2) * PI) + ((2 * PI) * (- 1)) < r2 by A3, A11;
then sin r2 > - 1 by A15, SIN_COS6:39;
then sin . r2 > - 1 by SIN_COS:def 17;
then A16: (sin . r2) " < (- 1) " by A14, XREAL_1:87;
cosec . r1 = 1 / (sin . (- (PI / 2))) by A4, A11, RFUNCT_1:def 2
.= 1 / (- 1) by SIN_COS:30, SIN_COS:76
.= - 1 ;
hence cosec . r2 < cosec . r1 by A7, A16, RFUNCT_1:def 2; :: thesis: verum

end;

suppose A17: - (PI / 2) < r1 ; :: thesis: cosec . r2 < cosec . r1

then - (PI / 2) < r2 by A3, XXREAL_0:2;
then r2 in ].(- (PI / 2)),0.[ by A9;
then A18: r2 in ].(- (PI / 2)),0.[ /\ (dom cosec) by A7, XBOOLE_0:def 4;
r1 in ].(- (PI / 2)),0.[ by A6, A17;
then r1 in ].(- (PI / 2)),0.[ /\ (dom cosec) by A4, XBOOLE_0:def 4;
hence cosec . r2 < cosec . r1 by A3, A18, Th15, RFUNCT_2:21; :: thesis: verum

end;

end;

end;

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

end;

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