let x be set ; :: thesis: ( x in [.(- 1),1.] implies arccot . x in [.(PI / 4),((3 / 4) * PI).] )
assume x in [.(- 1),1.] ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI).]
then x in ].(- 1),1.[ \/ {(- 1),1} by XXREAL_1:128;
then A1: ( x in ].(- 1),1.[ or x in {(- 1),1} ) by XBOOLE_0:def 3;

per cases ( x in ].(- 1),1.[ or x = - 1 or x = 1 ) by A1, TARSKI:def 2;

suppose A2: x in ].(- 1),1.[ ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI).]

then x in { s where s is Real : ( - 1 < s & s < 1 ) } by RCOMP_1:def 2;
then A3: ex s being Real st
( s = x & - 1 < s & s < 1 ) ;
A4: ].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
A5: [.(- 1),1.] /\ (dom arccot) = [.(- 1),1.] by Th24, XBOOLE_1:28;
then 1 in [.(- 1),1.] /\ (dom arccot) by XXREAL_1:1;
then A6: arccot . x > PI / 4 by A2, A5, A4, A3, Th40, Th48, RFUNCT_2:21;
- 1 in [.(- 1),1.] by XXREAL_1:1;
then (3 / 4) * PI > arccot . x by A2, A5, A4, A3, Th38, Th48, RFUNCT_2:21;
hence arccot . x in [.(PI / 4),((3 / 4) * PI).] by A6, XXREAL_1:1; :: thesis: verum

end;

suppose A7: x = - 1 ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI).]

PI / 4 < (PI / 4) * 3 by XREAL_1:155;
hence arccot . x in [.(PI / 4),((3 / 4) * PI).] by A7, Th38, XXREAL_1:1; :: thesis: verum

end;

suppose A8: x = 1 ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI).]

PI / 4 < (PI / 4) * 3 by XREAL_1:155;
hence arccot . x in [.(PI / 4),((3 / 4) * PI).] by A8, Th40, XXREAL_1:1; :: thesis: verum

end;

end;