let r, s be Element of RAT+ ; :: thesis: ( r = {} iff r + s = s )
s + {} = s by Th56;
hence ( r = {} iff r + s = s ) by Th69; :: thesis: verum