theorem :: WSIERP_1:7

for a, b, c being Nat st a gcd b = 1 & c gcd b = 1 holds
(a * c) gcd b = 1 by Th6;