theorem Th16: :: COMPTRIG:16

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