for x being Real st x in [.((3 / 2) * PI),(2 * PI).] holds
cos . x >= 0