for x being Real st x in ].(- (PI / 2)),0 .[ holds
diff cosec ,x < 0

proof

let x be Real; :: thesis: ( x in ].(- (PI / 2)),0 .[ implies diff cosec ,x < 0 )
assume A2: x in ].(- (PI / 2)),0 .[ ; :: thesis: diff cosec ,x < 0
].(- (PI / 2)),0 .[ \/ {(- (PI / 2))} = [.(- (PI / 2)),0 .[ by XXREAL_1:131;
then ].(- (PI / 2)),0 .[ c= [.(- (PI / 2)),0 .[ by XBOOLE_1:7;
then ].(- (PI / 2)),0 .[ c= ].(- PI ),0 .[ by Lm3, XBOOLE_1:1;
then ( - PI < x & x < 0 ) by A2, XXREAL_1:4;
then ( (- PI ) + (2 * PI ) < x + (2 * PI ) & x + (2 * PI ) < 0 + (2 * PI ) ) by XREAL_1:10;
then x + (2 * PI ) in ].PI ,(2 * PI ).[ ;
then sin . (x + (2 * PI )) < 0 by COMPTRIG:25;
then sin . x < 0 by SIN_COS:83;
then A3: (sin . x) ^2 > 0 ;
].(- (PI / 2)),0 .[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then cos . x > 0 by A2, COMPTRIG:27;
then (cos . x) / ((sin . x) ^2 ) > 0 / ((sin . x) ^2 ) by A3;
then - ((cos . x) / ((sin . x) ^2 )) < - 0 ;
hence diff cosec ,x < 0 by A2, Th7; :: thesis: verum

end;

hence cosec | ].(- (PI / 2)),0 .[ is decreasing by Th7, X3, ROLLE:10; :: thesis: verum