dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, RELAT_1:62;
hence rng arcsec1 = [.0,(PI / 2).[ by FUNCT_1:33; :: thesis: verum