for r being Real holds cos r <= 1