theorem Th15: :: COMPTRIG:15

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