theorem :: FUNCT_8:78
for A being symmetrical Subset of REAL holds - cos is_even_on A