let p, q be bag of SetPrimes ; :: thesis: ( p is prime-factorization-like & q is prime-factorization-like & support p misses support q implies Product p, Product q are_coprime )
assume that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: support p misses support q ; :: thesis: Product p, Product q are_coprime
assume not Product p, Product q are_coprime ; :: thesis: contradiction
then consider x being prime Nat such that
A4: x divides Product p and
A5: x divides Product q by PYTHTRIP:def 2;
A6: x in support q by A2, A5, Lm7;
x in support p by A1, A4, Lm7;
hence contradiction by A3, A6, XBOOLE_0:3; :: thesis: verum