set f = cos | [.0 ,PI .];
( (cos | [.0 ,PI .]) .: [.0 ,PI .] = [.(- 1),1.] & (((cos | [.0 ,PI .]) | [.0 ,PI .]) " ) | ((cos | [.0 ,PI .]) .: [.0 ,PI .]) is decreasing ) by Th49, COMPTRIG:41, FCONT_3:18, RELAT_1:162;
hence arccos | [.(- 1),1.] is decreasing by RELAT_1:101; :: thesis: verum