theorem Th54: :: ARYTM_3:54

for x being Element of RAT+ st x <> {} holds
ex y being Element of RAT+ st x *' y = 1