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