set f = cot | ].0,PI.[;
A1: (cot | ].0,PI.[) .: ].0,PI.[ =
rng ((cot | ].0,PI.[) | ].0,PI.[)
by RELAT_1:115
.=
rng (cot | ].0,PI.[)
by RELAT_1:73
.=
cot .: ].0,PI.[
by RELAT_1:115
;
(cot | ].0,PI.[) | ].0,PI.[ = cot | ].0,PI.[
by RELAT_1:73;
hence
arccot | (cot .: ].0,PI.[) is decreasing
by A1, Th8, FCONT_3:10; verum