theorem :: SINCOS10:129

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