theorem Th10: :: COMPTRIG:10

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