theorem :: SINCOS10:130

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