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