let x be Element of REAL+ ; :: thesis: ( x in omega implies for y being Element of REAL+ holds
( y in x iff ( y in omega & y <> x & y <=' x ) ) )
assume A1: x in omega ; :: thesis: for y being Element of REAL+ holds
( y in x iff ( y in omega & y <> x & y <=' x ) )
then A2: x c= omega by ORDINAL1:def 2;
reconsider m = x as Element of omega by A1;
reconsider x' = x as Element of RAT+ by A1, Lm5;
let y be Element of REAL+ ; :: thesis: ( y in x iff ( y in omega & y <> x & y <=' x ) )

hereby :: thesis: ( y in omega & y <> x & y <=' x implies y in x )

assume A3: y in x ; :: thesis: ( y in omega & y <> x & y <=' x )
hence y in omega by A2; :: thesis: ( y <> x & y <=' x )
then reconsider y' = y as Element of RAT+ by Lm5;
reconsider n = y as Element of omega by A2, A3;
thus y <> x by A3; :: thesis: y <=' x
n c= m by A3, ORDINAL1:def 2;
then consider C being Ordinal such that
A4: m = n +^ C by ORDINAL3:30;
C c= m by A4, ORDINAL3:27;
then reconsider C = C as Element of omega by ORDINAL1:22;
C in omega ;
then reconsider z' = C as Element of RAT+ by Lm5;
x' = y' + z' by A4, Lm45;
then y' <=' x' by ARYTM_3:def 13;
hence y <=' x by Lm14; :: thesis: verum

end;

assume A5: y in omega ; :: thesis: ( not y <> x or not y <=' x or y in x )
then reconsider n = y as Element of omega ;
reconsider y' = y as Element of RAT+ by A5, Lm5;
assume A6: y <> x ; :: thesis: ( not y <=' x or y in x )
assume y <=' x ; :: thesis: y in x
then y' <=' x' by Lm14;
then consider z' being Element of RAT+ such that
A7: y' + z' = x' by ARYTM_3:def 13;
reconsider k = z' as Element of omega by A1, A5, A7, ARYTM_3:78;
n +^ k = m by A7, Lm45;
then n c= m by ORDINAL3:27;
then n c< m by A6, XBOOLE_0:def 8;
hence y in x by ORDINAL1:21; :: thesis: verum