let x be Element of RAT+ ; :: thesis: x + {} = x
A1: ( (numerator x) *^ 1 = numerator x & {} *^ (denominator x) = {} ) by ORDINAL2:35, ORDINAL2:39;
A2: ( (denominator x) *^ 1 = denominator x & (numerator x) +^ {} = numerator x ) by ORDINAL2:27, ORDINAL2:39;
( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1;
hence x + {} = x by A1, A2, Th39; :: thesis: verum