set f = cot | ].0 ,PI .[;
A4: (cot | ].0 ,PI .[) | ].0 ,PI .[ = cot | ].0 ,PI .[ by RELAT_1:102;
A5: (cot | ].0 ,PI .[) | ].0 ,PI .[ is decreasing by Th8;
(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 ;
hence arccot | (cot .: ].0 ,PI .[) is decreasing by A4, A5, FCONT_3:18; :: thesis: verum