let x, y be Integer; :: thesis: ( ( x <> 0 or y <> 0 ) implies x div (x gcd y),y div (x gcd y) are_relative_prime )
assume A1: ( x <> 0 or y <> 0 ) ; :: thesis: x div (x gcd y),y div (x gcd y) are_relative_prime
then A2: x gcd y <> 0 by INT_2:35;
A3: ( x = (x div (x gcd y)) * (x gcd y) & y = (y div (x gcd y)) * (x gcd y) ) by Lm11, INT_2:31;
consider a, b being Integer such that
A4: ( x = (x gcd y) * a & y = (x gcd y) * b & a,b are_relative_prime ) by A1, INT_2:38;
( a = x div (x gcd y) & b = y div (x gcd y) ) by A2, A3, A4, XCMPLX_1:5;
hence x div (x gcd y),y div (x gcd y) are_relative_prime by A4; :: thesis: verum