theorem :: FUNCT_8:70

for A being symmetrical Subset of COMPLEX st A c= dom tan holds
tan is_odd_on A