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