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

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

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

A6: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then A7: tan | [.(- (PI / 4)),(PI / 4).] is increasing by Th7, RFUNCT_2:60;
- (PI / 4) in { s where s is Real : ( - (PI / 4) <= s & s <= PI / 4 ) } ;
then A8: - (PI / 4) in [.(- (PI / 4)),(PI / 4).] by RCOMP_1:def 1;
A9: [.(- (PI / 4)),(PI / 4).] /\ (dom tan ) = [.(- (PI / 4)),(PI / 4).] by A6, Th1, XBOOLE_1:1, XBOOLE_1:28;
A11: ].(- (PI / 4)),(PI / 4).[ c= [.(- (PI / 4)),(PI / 4).] by XXREAL_1:25;
x in { s where s is Real : ( - (PI / 4) < s & s < PI / 4 ) } by A4, RCOMP_1:def 2;
then ex s being Real st
( s = x & - (PI / 4) < s & s < PI / 4 ) ;
then A12: - 1 < tan . x by A4, A7, A8, A9, A11, Th15, RFUNCT_2:43;
PI / 4 in { s where s is Real : ( - (PI / 4) <= s & s <= PI / 4 ) } ;
then A13: PI / 4 in [.(- (PI / 4)),(PI / 4).] /\ (dom tan ) by A9, RCOMP_1:def 1;
x in { s where s is Real : ( - (PI / 4) < s & s < PI / 4 ) } by A4, RCOMP_1:def 2;
then ex s being Real st
( s = x & - (PI / 4) < s & s < PI / 4 ) ;
then tan . x < tan . (PI / 4) by A4, A7, A9, A11, A13, RFUNCT_2:43;
then tan . x < 1 by SIN_COS:def 32;
then tan . x in { s where s is Real : ( - 1 < s & s < 1 ) } by A12;
then A14: tan . x in ].(- 1),1.[ by RCOMP_1:def 2;
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
hence tan . x in [.(- 1),1.] by A14; :: thesis: verum

end;

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

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

end;

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

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

end;

end;