theorem Th63: :: SIN_COS9:63
for r being Real st - 1 <= r & r <= 1 holds
( - (PI / 4) <= arctan r & arctan r <= PI / 4 )