theorem Th22: :: COMPTRIG:22

cos | ].PI,(2 * PI).[ is increasing