for r being Real st - 1 <= r & r <= 1 & arctan r = - (PI / 4) holds
r = - 1 by Th17, Th51;