let r be Real; ( - 1 <= r & r <= 1 implies ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI ) )
assume that
A1:
- 1 <= r
and
A2:
r <= 1
; ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )
A3:
r in [.(- 1),1.]
by A1, A2, XXREAL_1:1;
then
r in dom (arccot | [.(- 1),1.])
by Th24, RELAT_1:62;
then
(arccot | [.(- 1),1.]) . r in rng (arccot | [.(- 1),1.])
by FUNCT_1:def 3;
then
arccot r in rng (arccot | [.(- 1),1.])
by A3, FUNCT_1:49;
hence
( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )
by Th56, XXREAL_1:1; verum