theorem :: FUNCT_8:69

for A being symmetrical Subset of COMPLEX st A c= ].(- (PI / 2)),(PI / 2).[ holds
tan is_odd_on A