theorem Th12: :: COMPTRIG:12

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