let A be symmetrical Subset of ; :: thesis: sin " is_odd_on A
A is symmetrical Subset of by NUMBERS:11, XBOOLE_1:1;
hence sin " is_odd_on A by Th18, Th65; :: thesis: verum