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