let p be Rational; :: thesis: denominator p = (denominator p) div ((numerator p) gcd (denominator p))
p = (numerator p) / (denominator p) by RAT_1:15;
hence denominator p = (denominator p) div ((numerator p) gcd (denominator p)) by Th15; :: thesis: verum