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; :: thesis: verum