let n be non zero Nat; :: thesis: ( n > 1 implies not Euler_factorization n is empty )
support (Euler_factorization n) c= dom (Euler_factorization n) by PRE_POLY:37;
hence ( n > 1 implies not Euler_factorization n is empty ) by Th22; :: thesis: verum