for A being symmetrical Subset of REAL holds sin is_odd_on A