theorem Th1: :: LEIBNIZ1:1

rng (tan | ].(- (PI / 2)),(PI / 2).[) = REAL