let x, y be Element of REAL+ ; :: thesis: ( x in omega & y in omega implies y + x in omega )
assume A1: ( x in omega & y in omega ) ; :: thesis: y + x in omega
then reconsider x0 = x, y0 = y as Element of omega ;
consider x9, y9 being Element of RAT+ such that
A2: ( x = x9 & y = y9 ) and
A3: x + y = x9 + y9 by A1, Lm5, Lm47;
x9 + y9 = x0 +^ y0 by A2, Lm45;
hence y + x in omega by A3, ORDINAL1:def 12; :: thesis: verum