set x0 = the Element of REAL+ ;
let X, Y be Subset of ; :: thesis: ( ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds
x <=' y ) implies ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y ) )
given x1 being Element of REAL+ such that A1: x1 in Y ; :: thesis: ( ex x, y being Element of REAL+ st
( x in X & y in Y & not x <=' y ) or ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y ) )
set Z = { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ;
assume A2: for x, y being Element of REAL+ st x in X & y in Y holds
x <=' y ; :: thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )

per cases ( ex z' being Element of RAT+ st
for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < z' ) or for z' being Element of RAT+ holds
not for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < z' ) ) ;

suppose ex z' being Element of RAT+ st
for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < z' ) ; :: thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )

then consider z' being Element of RAT+ such that
A3: for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < z' ) ;
z' in RAT+ ;
then reconsider z = z' as Element of REAL+ by Th1;
take z ; :: thesis: for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
let x, y be Element of REAL+ ; :: thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) )
assume that
A4: x in X and
A5: y in Y ; :: thesis: ( x <=' z & z <=' y )
thus x <=' z :: thesis: z <=' y

proof

assume z < x ; :: thesis: contradiction
then consider x0 being Element of REAL+ such that
A6: x0 in RAT+ and
A7: ( x0 < x & z < x0 ) by Lm30;
reconsider x' = x0 as Element of RAT+ by A6;
( z' < x' & x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ) by A4, A7, Lm14;
hence contradiction by A3; :: thesis: verum

end;

assume y < z ; :: thesis: contradiction
then consider y0 being Element of REAL+ such that
A8: y0 in RAT+ and
A9: y0 < z and
A10: y < y0 by Lm30;
reconsider y' = y0 as Element of RAT+ by A8;
y' < z' by A9, Lm14;
then y' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } by A3;
then ex y'' being Element of RAT+ st
( y' = y'' & ex x, z being Element of REAL+ st
( z = y'' & x in X & z < x ) ) ;
then consider x1, y1 being Element of REAL+ such that
A11: y1 = y' and
A12: x1 in X and
A13: y1 < x1 ;
y < x1 by A10, A11, A13, Lm31;
hence contradiction by A2, A5, A12; :: thesis: verum

end;

suppose A14: for z' being Element of RAT+ holds
not for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < z' ) ; :: thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )

A15: now

assume { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: contradiction
then consider t being Element of RAT+ such that
A16: { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } = { s where s is Element of RAT+ : s < t } and
t <> {} ;
for x' being Element of RAT+ holds
( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < t )

proof

let x' be Element of RAT+ ; :: thesis: ( x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } iff x' < t )

hereby :: thesis: ( x' < t implies x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } )

assume x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ; :: thesis: x' < t
then ex s being Element of RAT+ st
( s = x' & s < t ) by A16;
hence x' < t ; :: thesis: verum

end;

thus ( x' < t implies x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ) by A16; :: thesis: verum

end;

hence contradiction by A14; :: thesis: verum

end;

A17: { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } c= RAT+

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } or e in RAT+ )
assume e in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ; :: thesis: e in RAT+
then ex z' being Element of RAT+ st
( e = z' & ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) ) ;
hence e in RAT+ ; :: thesis: verum

end;

now

assume { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } = {} ; :: thesis: contradiction
then A18: for x' being Element of RAT+ st x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } holds
x' < {} ;
for x' being Element of RAT+ st x' < {} holds
x' in { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } by ARYTM_3:71;
hence contradiction by A14, A18; :: thesis: verum

end;

then reconsider Z = { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } as non empty Subset of by A17;

A19: now

assume A20: Z = RAT+ ; :: thesis: contradiction

per cases ( x1 in RAT+ or not x1 in RAT+ ) ;

suppose x1 in RAT+ ; :: thesis: contradiction

then reconsider x' = x1 as Element of RAT+ ;
x' in Z by A20;
then ex z' being Element of RAT+ st
( x' = z' & ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) ) ;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose A21: not x1 in RAT+ ; :: thesis: contradiction

x1 in REAL+ ;
then x1 in { A where A is Subset of : 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 A21, Lm3, XBOOLE_0:def 3;
then consider A being Subset of such that
A22: x1 = A and
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 ) ) ;
x1 <> RAT+ by Lm28;
then consider x' being Element of RAT+ such that
A23: not x' in A by A22, SUBSET_1:49;
x' in RAT+ ;
then reconsider x2 = x' as Element of REAL+ by Th1;
x2 in Z by A20;
then ex z' being Element of RAT+ st
( x' = z' & ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) ) ;
then consider x being Element of REAL+ such that
A24: x in X and
A25: x2 < x ;
x1 < x2 by A21, A22, A23, Def5;
then x1 < x by A25, Lm31;
hence contradiction by A1, A2, A24; :: thesis: verum

end;

end;

end;

for t being Element of RAT+ st t in Z holds
( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) )

proof

let t be Element of RAT+ ; :: thesis: ( t in Z implies ( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) ) )
t in RAT+ ;
then reconsider y0 = t as Element of REAL+ by Th1;
assume t in Z ; :: thesis: ( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) )
then ex z' being Element of RAT+ st
( z' = t & ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) ) ;
then consider x0 being Element of REAL+ such that
A26: x0 in X and
A27: y0 < x0 ;
thus for s being Element of RAT+ st s <=' t holds
s in Z :: thesis: ex s being Element of RAT+ st
( s in Z & t < s )

proof

let s be Element of RAT+ ; :: thesis: ( s <=' t implies s in Z )
s in RAT+ ;
then reconsider z = s as Element of REAL+ by Th1;
assume s <=' t ; :: thesis: s in Z
then z <=' y0 by Lm14;
then z < x0 by A27, Lm31;
hence s in Z by A26; :: thesis: verum

end;

consider z being Element of REAL+ such that
A28: z in RAT+ and
A29: z < x0 and
A30: y0 < z by A27, Lm30;
reconsider z' = z as Element of RAT+ by A28;
take z' ; :: thesis: ( z' in Z & t < z' )
thus z' in Z by A26, A29; :: thesis: t < z'
thus t < z' by A30, Lm14; :: thesis: verum

end;

then Z in { A where A is Subset of : 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 ) ) } ;
then A31: Z in { A where A is Subset of : 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 ) ) } \ {RAT+ } by A19, ZFMISC_1:64;
then Z in ({ A where A is Subset of : 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 ) ) } \ {RAT+ }) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15, XBOOLE_0:def 5;
then reconsider z = Z as Element of REAL+ by Lm4;
take z ; :: thesis: for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
let x, y be Element of REAL+ ; :: thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) )
assume that
A32: x in X and
A33: y in Y ; :: thesis: ( x <=' z & z <=' y )

A34: now

assume z in RAT+ ; :: thesis: contradiction
then z in {{} } by A31, Lm9, XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

hereby :: thesis: z <=' y

assume z < x ; :: thesis: contradiction
then consider x0 being Element of REAL+ such that
A35: x0 in RAT+ and
A36: x0 < x and
A37: z < x0 by Lm30;
reconsider x' = x0 as Element of RAT+ by A35;
x' in z by A32, A36;
hence contradiction by A34, A37, Def5; :: thesis: verum

end;

assume y < z ; :: thesis: contradiction
then consider y0 being Element of REAL+ such that
A38: y0 in RAT+ and
A39: y0 < z and
A40: y < y0 by Lm30;
reconsider y' = y0 as Element of RAT+ by A38;
y' in z by A34, A39, Def5;
then ex z' being Element of RAT+ st
( y' = z' & ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) ) ;
then consider x0 being Element of REAL+ such that
A41: x0 in X and
A42: y0 < x0 ;
y < x0 by A40, A42, Lm31;
hence contradiction by A2, A33, A41; :: thesis: verum

end;

end;