let x, y be Element of REAL+ ; :: thesis:
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:
thus ( y in RAT+ & x in RAT+ implies ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 ) ) :: thesis:

assume ( y in RAT+ & x in RAT+ ) ; :: thesis:
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:

end;

thus ( y in RAT+ & not x in RAT+ implies y in x ) by A1; :: thesis:
thus ( not y in RAT+ & x in RAT+ implies not x in y ) by A1; :: thesis:
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 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: