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