theorem Th64: :: ARYTM_3:64

for s being Element of RAT+ holds {} <=' s