let x be Element of RAT+ ; :: thesis: x + {} = x
A1: ( (numerator x) *^ 1 = numerator x & {} *^ (denominator x) = {} ) by ORDINAL2:52, ORDINAL2:56;
A2: ( (denominator x) *^ 1 = denominator x & (numerator x) +^ {} = numerator x ) by ORDINAL2:44, ORDINAL2:56;
( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1;
hence x + {} = x by A1, A2, Th45; :: thesis: verum