let s be Element of RAT+ ; :: thesis: ( s <=' {} implies s = {} )
assume ex r being Element of RAT+ st {} = s + r ; :: according to ARYTM_3:def 13 :: thesis: s = {}
hence s = {} by Th70; :: thesis: verum