theorem Th1: :: SIN_COS9:1

].(- (PI / 2)),(PI / 2).[ c= dom tan