theorem Th32: :: COMPTRIG:32

rng (cos | [.0,PI.]) = [.(- 1),1.]