X: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
A2: [.(- 1),1.] = cot .: [.(PI / 4),((3 / 4) * PI ).] by Th20, RELAT_1:148;
[.(- 1),1.] c= cot .: ].0 ,PI .[ by A2, X, RELAT_1:156;
hence arccot | [.(- 1),1.] is decreasing by Th44, RFUNCT_2:61; :: thesis: verum