let x be set ; :: thesis: ( x in [.(PI / 4),((3 / 4) * PI ).] implies cot . x in [.(- 1),1.] )
PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
then A1: (PI / 4) * 3 > PI / 4 by XREAL_1:157;
assume x in [.(PI / 4),((3 / 4) * PI ).] ; :: thesis: cot . x in [.(- 1),1.]
then x in ].(PI / 4),((3 / 4) * PI ).[ \/ {(PI / 4),((3 / 4) * PI )} by A1, XXREAL_1:128;
then A2: ( x in ].(PI / 4),((3 / 4) * PI ).[ or x in {(PI / 4),((3 / 4) * PI )} ) by XBOOLE_0:def 3;

per cases ( x in ].(PI / 4),((3 / 4) * PI ).[ or x = PI / 4 or x = (3 / 4) * PI ) by A2, TARSKI:def 2;

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

then x in { s where s is Real : ( PI / 4 < s & s < (3 / 4) * PI ) } by RCOMP_1:def 2;
then A4: ex s being Real st
( s = x & PI / 4 < s & s < (3 / 4) * PI ) ;
A5: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
then A6: cot | [.(PI / 4),((3 / 4) * PI ).] is decreasing by Th8, RFUNCT_2:61;
x in { s where s is Real : ( PI / 4 < s & s < (3 / 4) * PI ) } by A3, RCOMP_1:def 2;
then A7: ex s being Real st
( s = x & PI / 4 < s & s < (3 / 4) * PI ) ;
A8: ].(PI / 4),((3 / 4) * PI ).[ c= [.(PI / 4),((3 / 4) * PI ).] by XXREAL_1:25;
A9: [.(PI / 4),((3 / 4) * PI ).] /\ (dom cot ) = [.(PI / 4),((3 / 4) * PI ).] by A5, Th2, XBOOLE_1:1, XBOOLE_1:28;
(3 / 4) * PI in { s where s is Real : ( PI / 4 <= s & s <= (3 / 4) * PI ) } by A1;
then (3 / 4) * PI in [.(PI / 4),((3 / 4) * PI ).] /\ (dom cot ) by A9, RCOMP_1:def 1;
then A10: - 1 < cot . x by A3, A6, A9, A8, A7, Th18, RFUNCT_2:44;
PI / 4 in { s where s is Real : ( PI / 4 <= s & s <= (3 / 4) * PI ) } by A1;
then PI / 4 in [.(PI / 4),((3 / 4) * PI ).] /\ (dom cot ) by A9, RCOMP_1:def 1;
then cot . x < 1 by A3, A6, A9, A8, A4, Th18, RFUNCT_2:44;
then cot . x in { s where s is Real : ( - 1 < s & s < 1 ) } by A10;
then A11: cot . x in ].(- 1),1.[ by RCOMP_1:def 2;
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
hence cot . x in [.(- 1),1.] by A11; :: thesis: verum

end;

suppose x = PI / 4 ; :: thesis: cot . x in [.(- 1),1.]

then cot . x in { s where s is Real : ( - 1 <= s & s <= 1 ) } by Th18;
hence cot . x in [.(- 1),1.] by RCOMP_1:def 1; :: thesis: verum

end;

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

then cot . x in { s where s is Real : ( - 1 <= s & s <= 1 ) } by Th18;
hence cot . x in [.(- 1),1.] by RCOMP_1:def 1; :: thesis: verum

end;

end;