theorem :: SIN_COS2:3

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