let x be set ; :: thesis: ( x in [.(PI / 4),((3 / 4) * PI ).] implies cot . x in [.(- 1),1.] )
assume A1: x in [.(PI / 4),((3 / 4) * PI ).] ; :: thesis: cot . x in [.(- 1),1.]
A2: PI / 4 <= (3 / 4) * PI

proof

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 (PI / 4) * 3 > PI / 4 by XREAL_1:157;
hence PI / 4 <= (3 / 4) * PI ; :: thesis: verum

end;

x in ].(PI / 4),((3 / 4) * PI ).[ \/ {(PI / 4),((3 / 4) * PI )} by A1, A2, XXREAL_1:128;
then A3: ( 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 A3, TARSKI:def 2;

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

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

end;

end;