:: deftheorem defines numerator RAT_1:def 4 :
for p being Rational holds numerator p = (denominator p) * p;