let q be Rational; :: thesis: numerator q, denominator q are_relative_prime
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 by INT_1:def 3;
(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;
denominator q <> 0 by RAT_1:def 3;
then 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_relative_prime ; :: 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