A1: [.(- 1),1.] = cot .: [.(PI / 4),((3 / 4) * PI).] by Th22, RELAT_1:148;
[.(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:156, RFUNCT_2:61; :: thesis: verum