theorem :: FUNCT_8:64

for A being symmetrical Subset of REAL holds absreal is_even_on A