X: ].0 ,PI .[ c= dom cot by Lm2, FDIFF_1:def 7;
PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: PI > 0 by XXREAL_1:4;
for x being Real st x in ].0 ,PI .[ holds
diff cot ,x < 0

proof

let x be Real; :: thesis: ( x in ].0 ,PI .[ implies diff cot ,x < 0 )
assume A3: x in ].0 ,PI .[ ; :: thesis: diff cot ,x < 0
then 0 < sin . x by COMPTRIG:23;
then (sin . x) ^2 > 0 by SQUARE_1:74;
then 1 / ((sin . x) ^2 ) > 0 / ((sin . x) ^2 ) by XREAL_1:76;
then - (1 / ((sin . x) ^2 )) < - 0 by XREAL_1:26;
hence diff cot ,x < 0 by A3, Lm4; :: thesis: verum

end;

hence cot | ].0 ,PI .[ is decreasing by A1, Lm2, X, ROLLE:10; :: thesis: verum