let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI ) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then r in dom (arccot | [.(- 1),1.]) by Th22, RELAT_1:91;
then (arccot | [.(- 1),1.]) . r in rng (arccot | [.(- 1),1.]) by FUNCT_1:def 5;
then arccot r in rng (arccot | [.(- 1),1.]) by A1, FUNCT_1:72;
hence ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI ) by Th54, XXREAL_1:1; :: thesis: verum