theorem Th25: :: COMPTRIG:25

cos | [.0,PI.] is decreasing