theorem :: NUMBER04:11

for a, b, c being Nat st ( a <> 0 or b <> 0 ) & c <> 0 & a,b,c are_mutually_coprime holds
a * b,c are_coprime by EULER_1:14;