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