let q be Rational; :: thesis: numerator q, denominator q are_coprime
set k = numerator q;
set h = denominator q;
reconsider a = (numerator q) gcd (denominator q) as Element of NAT by INT_2:20;
a divides numerator q by INT_2:21;
then A1: ex l being Integer st numerator q = a * l ;
(numerator q) gcd (denominator q) divides denominator q by INT_2:21;
then consider b being Nat such that
A2: denominator q = a * b by NAT_D:def 3;
a <> 0 by INT_2:5;
then A3: a >= 0 + 1 by NAT_1:13;
reconsider b = b as Element of NAT by ORDINAL1:def 12;
A4: denominator q = a * b by A2;
assume not numerator q, denominator q are_coprime ; :: thesis: contradiction
then a <> 1 by INT_2:def 3;
then a > 1 by A3, XXREAL_0:1;
hence contradiction by A1, A4, RAT_1:29; :: thesis: verum