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

proof

let x be Real; :: thesis: ( x in ].0 ,(PI / 2).[ implies diff cosec ,x < 0 )
assume A2: x in ].0 ,(PI / 2).[ ; :: thesis: diff cosec ,x < 0
].0 ,(PI / 2).[ c= ].0 ,PI .[ by COMPTRIG:21, XXREAL_1:46;
then sin . x > 0 by A2, COMPTRIG:23;
then A3: (sin . x) ^2 > 0 ;
].0 ,(PI / 2).[ 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, Th8; :: thesis: verum

end;

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