dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, RELAT_1:62;
hence rng arcsec2 = ].(PI / 2),PI.] by FUNCT_1:33; :: thesis: verum