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:25, FCONT_3:10, RELAT_1:129;
hence arccos | [.(- 1),1.] is decreasing by RELAT_1:72; :: thesis: verum