theorem Th53: :: ARYTM_3:53

for x being Element of RAT+ holds x *' one = x