let A be symmetrical Subset of REAL; :: thesis: cos ^2 is_even_on A
( A is symmetrical Subset of COMPLEX & cos is_even_on A ) by Th66, NUMBERS:11, XBOOLE_1:1;
hence cos ^2 is_even_on A by Th23; :: thesis: verum