let X, Y be Subset of REAL+ ; :: thesis: ( ex x being Element of REAL+ st x in X & 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 x0 being Element of REAL+ such that x0 in X ; :: thesis: ( for x being Element of REAL+ holds not x in Y or 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 ) )
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 ) )
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 )
set Z = { z' where z' is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z' & x in X & z < x ) } ;
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 and
A8: z < x0 by Lm30;
reconsider x' = x0 as Element of RAT+ by A6;
A9: z' < x' by A8, Lm14;
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;
hence contradiction by A3, A9; :: thesis: verum
end;
assume y < z ; :: thesis: contradiction
then consider y0 being Element of REAL+ such that
A10: y0 in RAT+ and
A11: y0 < z and
A12: y < y0 by Lm30;
reconsider y' = y0 as Element of RAT+ by A10;
y' < z' by A11, 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
A13: y1 = y' and
A14: x1 in X and
A15: y1 < x1 ;
y < x1 by A12, A13, A15, Lm31;
hence contradiction by A2, A5, A14; :: thesis: verum
end;
suppose A16: 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 )
A17: 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
A18: { 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 A18;
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 A18; :: thesis: verum
end;
hence contradiction by A16; :: thesis: verum
end;
A19: 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 A20: 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 A16, A20; :: thesis: verum
end;
{ 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;
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 RAT+ by A19;
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
A21: x0 in X and
A22: 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 A22, Lm31;
hence s in Z by A21; :: thesis: verum
end;
consider z being Element of REAL+ such that
A23: z in RAT+ and
A24: z < x0 and
A25: y0 < z by A22, Lm30;
reconsider z' = z as Element of RAT+ by A23;
take z' ; :: thesis: ( z' in Z & t < z' )
thus z' in Z by A21, A24; :: thesis: t < z'
thus t < z' by A25, Lm14; :: thesis: verum
end;
then A26: 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 ) ) } ;
now
assume A27: 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 A27;
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 A28: 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 A28, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A29: 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
A30: not x' in A by A29, SUBSET_1:49;
x' in RAT+ ;
then reconsider x2 = x' as Element of REAL+ by Th1;
A31: x1 < x2 by A28, A29, A30, Def5;
x2 in Z by A27;
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
A32: x in X and
A33: x2 < x ;
x1 < x by A31, A33, Lm31;
hence contradiction by A1, A2, A32; :: thesis: verum
end;
end;
end;
then A34: 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 A26, ZFMISC_1:64;
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 A17, 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
A36: x in X and
A37: y in Y ; :: thesis: ( x <=' z & z <=' y )
hereby :: thesis: z <=' y
assume z < x ; :: thesis: contradiction
then consider x0 being Element of REAL+ such that
A38: x0 in RAT+ and
A39: x0 < x and
A40: z < x0 by Lm30;
reconsider x' = x0 as Element of RAT+ by A38;
x' in z by A36, A39;
hence contradiction by A35, A40, Def5; :: thesis: verum
end;
assume y < z ; :: thesis: contradiction
then consider y0 being Element of REAL+ such that
A41: y0 in RAT+ and
A42: y0 < z and
A43: y < y0 by Lm30;
reconsider y' = y0 as Element of RAT+ by A41;
y' in z by A35, A42, 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
A44: x0 in X and
A45: y0 < x0 ;
y < x0 by A43, A45, Lm31;
hence contradiction by A2, A37, A44; :: thesis: verum
end;
end;