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