X: ].0 ,PI .[ c= dom cot by Th2;
for x0 being Real st x0 in ].0 ,PI .[ holds
diff cot ,x0 < 0

proof

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

end;

then rng (cot | ].0 ,PI .[) is open by Lm2, X, FDIFF_2:41;
hence dom arccot is open by FUNCT_1:55; :: thesis: verum