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; verum