dom (Euler_factorization_2 n) = support (ppf n) by Def3;
hence dom (Euler_factorization_2 n) c= SetPrimes ; :: according to RELAT_1:def 18 :: thesis: verum