theorem Th11: :: COMPTRIG:11

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