( - (PI / 2) < - (PI / 4) & - (PI / 4) < PI / 2 ) by Lm7, XXREAL_1:4;
then arctan (- 1) = - (PI / 4) by Th15, Th33;
hence ( arctan (- 1) = - (PI / 4) & arctan . (- 1) = - (PI / 4) ) ; :: thesis: verum