theorem :: FUNCT_8:74
for A being symmetrical Subset of REAL holds |.cos.| is_even_on A