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