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