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

proof

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),0 .[ implies diff cosec ,x0 < 0 )
assume A1: x0 in ].(- (PI / 2)),0 .[ ; :: thesis: diff cosec ,x0 < 0
then x0 < 0 by XXREAL_1:4;
then A2: x0 + (2 * PI ) < 0 + (2 * PI ) by XREAL_1:10;
].(- (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 < x0 by A1, XXREAL_1:4;
then (- PI ) + (2 * PI ) < x0 + (2 * PI ) by XREAL_1:10;
then x0 + (2 * PI ) in ].PI ,(2 * PI ).[ by A2;
then sin . (x0 + (2 * PI )) < 0 by COMPTRIG:25;
then A3: sin . x0 < 0 by SIN_COS:83;
].(- (PI / 2)),0 .[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then cos . x0 > 0 by A1, COMPTRIG:27;
then - ((cos . x0) / ((sin . x0) ^2 )) < - 0 by A3;
hence diff cosec ,x0 < 0 by A1, Th7; :: thesis: verum

end;

then rng (cosec | ].(- (PI / 2)),0 .[) is open by Lm16, Th7, FDIFF_2:41;
hence cosec .: ].(- (PI / 2)),0 .[ is open by RELAT_1:148; :: thesis: verum