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 A1: x in ].0,(PI / 2).[ ; :: thesis: diff (cosec,x) < 0
].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then A2: cos . x > 0 by A1, COMPTRIG:11;
].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46;
then sin . x > 0 by A1, COMPTRIG:7;
then - ((cos . x) / ((sin . x) ^2)) < - 0 by A2;
hence diff (cosec,x) < 0 by A1, Th8; :: thesis: verum

end;

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