for x being Real st x in [.PI,(2 * PI).] holds
sin . x <= 0