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 A1: x0 in ].0,PI.[ ; :: thesis: diff (cot,x0) < 0
then 0 < sin . x0 by COMPTRIG:7;
then (sin . x0) ^2 > 0 ;
then 1 / ((sin . x0) ^2) > 0 / ((sin . x0) ^2) ;
then - (1 / ((sin . x0) ^2)) < - 0 ;
hence diff (cot,x0) < 0 by A1, Lm4; :: thesis: verum
end;
then rng (cot | ].0,PI.[) is open by Lm2, Th2, FDIFF_2:41;
hence dom arccot is open by FUNCT_1:33; :: thesis: verum