for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like holds
( x divides Product p iff x in support p ) by Lm4, Lm7;