theorem Th9: :: COMPTRIG:9

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