for r being Real st 0 <= r holds
sin . r <= r