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