let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( - (PI / 4) < arctan r & arctan r < PI / 4 ) )
assume A1: ( - 1 < r & r < 1 ) ; :: thesis: ( - (PI / 4) < arctan r & arctan r < PI / 4 )
then ( - (PI / 4) <= arctan r & arctan r <= PI / 4 ) by Th61;
then A2: ( ( - (PI / 4) < arctan r & arctan r < PI / 4 ) or - (PI / 4) = arctan r or arctan r = PI / 4 ) by XXREAL_0:1;
tan (PI / 4) = tan . (PI / 4) by Lm8, Th13
.= 1 by SIN_COS:def 32 ;
hence ( - (PI / 4) < arctan r & arctan r < PI / 4 ) by A1, A2, Th15, Th49; :: thesis: verum