theorem Th13: :: COMPTRIG:13

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