for x being Element of RAT+ holds (numerator x) / (denominator x) = x