let X, Y be Subset of REAL+; :: 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 = { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & 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 z9 being Element of RAT+ st
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) or for z9 being Element of RAT+ holds
not for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ) ;

suppose ex z9 being Element of RAT+ st
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; :: 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 z9 being Element of RAT+ such that
A3: for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ;
reconsider z = z9 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 x9 = x0 as Element of RAT+ by A6;
( z9 < x9 & x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & 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 y9 = y0 as Element of RAT+ by A8;
y9 < z9 by A9, Lm14;
then y9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } by A3;
then ex y99 being Element of RAT+ st
( y9 = y99 & ex x, z being Element of REAL+ st
( z = y99 & x in X & z < x ) ) ;
then consider x1, y1 being Element of REAL+ such that
A11: y1 = y9 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 z9 being Element of RAT+ holds
not for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; :: 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 :: thesis: not { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }

assume { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & 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: { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } = { s where s is Element of RAT+ : s < t } and
t <> {} ;
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < t )

proof

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

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

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

end;

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

end;

hence contradiction by A14; :: thesis: verum

end;

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

proof

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

end;

now :: thesis: not { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } = {}

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

end;

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

A19: now :: thesis: not Z = RAT+

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

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

suppose x1 in RAT+ ; :: thesis: contradiction

then reconsider x9 = x1 as Element of RAT+ ;
x9 in Z by A20;
then ex z9 being Element of RAT+ st
( x9 = z9 & ex x, z being Element of REAL+ st
( z = z9 & 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 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 A21, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ 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 x9 being Element of RAT+ such that
A23: not x9 in A by A22, SUBSET_1:28;
reconsider x2 = x9 as Element of REAL+ by Th1;
x2 in Z by A20;
then ex z9 being Element of RAT+ st
( x9 = z9 & ex x, z being Element of REAL+ st
( z = z9 & 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 ) ) )
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 z9 being Element of RAT+ st
( z9 = t & ex x, z being Element of REAL+ st
( z = z9 & 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 )
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 z9 = z as Element of RAT+ by A28;
take z9 ; :: thesis: ( z9 in Z & t < z9 )
thus z9 in Z by A26, A29; :: thesis: t < z9
thus t < z9 by A30, Lm14; :: thesis: verum

end;

then Z 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 ) ) } ;
then A31: Z 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 ) ) } \ {RAT+} by A19, ZFMISC_1:56;
then Z 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 ) ) } \ {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 :: thesis: not z in RAT+

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 x9 = x0 as Element of RAT+ by A35;
x9 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 y9 = y0 as Element of RAT+ by A38;
y9 in z by A34, A39, Def5;
then ex z9 being Element of RAT+ st
( y9 = z9 & ex x, z being Element of REAL+ st
( z = z9 & 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;