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