set f = cot | ].0,PI.[;
A1: (cot | ].0,PI.[) .: ].0,PI.[ = rng ((cot | ].0,PI.[) | ].0,PI.[) by RELAT_1:148
.= rng (cot | ].0,PI.[) by RELAT_1:102
.= cot .: ].0,PI.[ by RELAT_1:148 ;
(cot | ].0,PI.[) | ].0,PI.[ = cot | ].0,PI.[ by RELAT_1:102;
hence arccot | (cot .: ].0,PI.[) is decreasing by A1, Th8, FCONT_3:18; :: thesis: verum