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