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