let s be Element of RAT+ ; :: thesis: {} <=' s
take s ; :: according to ARYTM_3:def 13 :: thesis: s = {} + s
thus s = {} + s by Th50; :: thesis: verum