theorem :: FUNCT_8:72

for A being symmetrical Subset of COMPLEX st A c= [.(- 1),1.] holds
arctan is_odd_on A