theorem Th18: :: NUMBER03:18

for a, b being Nat st ( a <> 0 or b <> 0 ) holds
ex A, B being Nat st
( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime )