theorem Th39: :: ARYTM_3:39

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