for r being Real holds - 1 <= cos r