theorem Th14: :: COMPTRIG:14

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