Product m > 0 by x0;
then Product m is Element of NAT by INT_1:16;
hence ( Product m is positive & Product m is natural ) by x0; :: thesis: verum