let x, y be Element of REAL+ ; :: thesis: ( ( ( x in RAT+ & y in RAT+ & ( for x', y' being Element of RAT+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) 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 x', y' being Element of RAT+ st
( y = x' & x = y' & x' <=' y' ) ) & ( 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 x', y' being Element of RAT+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) 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 x', y' being Element of RAT+ st
( y = x' & x = y' & x' <=' y' ) ) & ( 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 y', x' being Element of RAT+ st
( y = y' & x = x' & y' <=' x' ) ) :: 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 y', x' being Element of RAT+ st
( y = y' & x = x' & y' <=' x' )
then reconsider y' = y, x' = x as Element of RAT+ ;
y' <=' x' by A1;
hence ex y', x' being Element of RAT+ st
( y = y' & x = x' & y' <=' x' ) ; :: 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
( x in REAL+ & y 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 ) ) } & 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;
hence y c= x by A1, A2, Lm13; :: thesis: verum