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