theorem Th20: :: COMPTRIG:20

sin | ].(PI / 2),((3 / 2) * PI).[ is decreasing