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 reconsider m = x as Element of omega ;
reconsider x9 = 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 ) )
A2: x c= omega by A1, ORDINAL1:def 2;
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 )
then reconsider n = y as Element of omega by A2;
thus y in omega by A2, A3; :: thesis: ( y <> x & y <=' x )
then reconsider y9 = y as Element of RAT+ by Lm5;
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:27;
C c= m by A4, ORDINAL3:24;
then reconsider C = C as Element of omega by ORDINAL1:12;
reconsider z9 = C as Element of RAT+ by Lm5;
x9 = y9 + z9 by A4, Lm45;
then y9 <=' x9 ;
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 y9 = y as Element of RAT+ by Lm5;
reconsider n = y as Element of omega by A5;
assume A6: y <> x ; :: thesis: ( not y <=' x or y in x )
assume y <=' x ; :: thesis: y in x
then y9 <=' x9 by Lm14;
then consider z9 being Element of RAT+ such that
A7: y9 + z9 = x9 ;
reconsider k = z9 as Element of omega by A1, A5, A7, ARYTM_3:71;
n +^ k = m by A7, Lm45;
then n c= m by ORDINAL3:24;
then n c< m by A6;
hence y in x by ORDINAL1:11; :: thesis: verum