A1: [.(- 1),1.] = cot .: [.(PI / 4),((3 / 4) * PI).] by Th22, RELAT_1:115;
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[ by Lm9, Lm10, XXREAL_2:def 12;
hence arccot | [.(- 1),1.] is decreasing by A1, Th46, RELAT_1:123, RFUNCT_2:29; :: thesis: verum