theorem Th66: :: SINCOS10:66
arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39;