theorem Th6: :: EULER_1:6

for a, b, c being Nat st a <> 0 & c <> 0 & (a * c) gcd (b * c) = c holds
a,b are_coprime