theorem :: FUNCT_8:60

for A being symmetrical Subset of REAL holds signum is_odd_on A