for B being symmetrical Subset of REAL st ( for x being Real st x in B holds
cos . x <> 0 ) holds
sec is_even_on B