theorem :: ARYTM_3:65

for s being Element of RAT+ st s <=' {} holds
s = {} by Th63;