theorem :: SINCOS10:10

sec | ].(PI / 2),PI.[ is continuous by Th6, FDIFF_1:25;