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 x', y' being Element of RAT+ such that
A2: x = x' and
A3: y = y' and
A4: x + y = x' + y' by A1, Lm5, Lm47;
x' + y' = x0 +^ y0 by A2, A3, Lm45;
hence y + x in omega by A4, ORDINAL1:def 13; :: thesis: verum