let A be symmetrical Subset of REAL ; :: thesis: - cos is_even_on A
A is symmetrical Subset of COMPLEX by XBOOLE_1:1, NUMBERS:11;
hence - cos is_even_on A by Th13, Th55; :: thesis: verum