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