theorem Th21: :: SIN_COS9:21

rng (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- 1),1.]