let x, y be Element of REAL+ ; :: thesis: ( ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) implies ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) )
assume A1: ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( not ( x in RAT+ & y in RAT+ ) & not ( x in RAT+ & not y in RAT+ ) & not ( not x in RAT+ & y in RAT+ ) & not x c= y ) ) ; :: thesis: ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
thus ( y in RAT+ & x in RAT+ implies ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 ) ) :: thesis: ( ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )

proof

assume ( y in RAT+ & x in RAT+ ) ; :: thesis: ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 )
then reconsider y9 = y, x9 = x as Element of RAT+ ;
y9 <=' x9 by A1;
hence ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 ) ; :: thesis: verum

end;

thus ( y in RAT+ & not x in RAT+ implies y in x ) by A1; :: thesis: ( ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
thus ( not y in RAT+ & x in RAT+ implies not x in y ) by A1; :: thesis: ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x )
assume A2: ( not ( y in RAT+ & x in RAT+ ) & not ( y in RAT+ & not x in RAT+ ) & not ( not y in RAT+ & x in RAT+ ) ) ; :: thesis: y c= x
y in REAL+ ;
then A3: y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A2, Lm3, XBOOLE_0:def 3;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A2, Lm3, XBOOLE_0:def 3;
hence y c= x by A1, A2, A3, Lm13; :: thesis: verum