let X, Y be Subset of REAL; :: thesis: ( ( for x, y being Real st x in X & y in Y holds
x <= y ) implies ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y ) )
assume A1: for x, y being Real st x in X & y in Y holds
x <= y ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
per cases ( X = 0 or Y = 0 or ( X <> 0 & Y <> 0 ) ) ;
suppose A2: ( X = 0 or Y = 0 ) ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
take 1 ; :: thesis: for x, y being Real st x in X & y in Y holds
( x <= 1 & 1 <= y )
thus for x, y being Real st x in X & y in Y holds
( x <= 1 & 1 <= y ) by A2; :: thesis: verum
end;
suppose that A3: X <> 0 and
A4: Y <> 0 ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
consider x1 being Element of REAL such that
A5: x1 in X by A3, SUBSET_1:4;
A6: X c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1, XBOOLE_1:1;
A7: Y c= REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1, XBOOLE_1:1;
A8: ex x2 being Element of REAL st x2 in Y by A4, SUBSET_1:4;
thus ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y ) :: thesis: verum
proof
per cases ( ( X misses REAL+ & Y misses [:{0},REAL+:] ) or Y meets [:{0},REAL+:] or X meets REAL+ ) ;
suppose that A9: X misses REAL+ and
A10: Y misses [:{0},REAL+:] ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
take z = 0 ; :: thesis: for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
let x, y be Real; :: thesis: ( x in X & y in Y implies ( x <= z & z <= y ) )
assume that
A11: x in X and
A12: y in Y ; :: thesis: ( x <= z & z <= y )
( not z in [:{0},REAL+:] & not x in REAL+ ) by A9, A11, ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3;
hence x <= z by XXREAL_0:def 5; :: thesis: z <= y
Y c= REAL+ by A7, A10, XBOOLE_1:73;
then reconsider y9 = y, o = 0 as Element of REAL+ by A12, ARYTM_2:20;
o <=' y9 by ARYTM_1:6;
hence z <= y by Lm1; :: thesis: verum
end;
suppose A13: Y meets [:{0},REAL+:] ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
{ r where r is Element of REAL+ : [0,r] in X } c= REAL+
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { r where r is Element of REAL+ : [0,r] in X } or u in REAL+ )
assume u in { r where r is Element of REAL+ : [0,r] in X } ; :: thesis: u in REAL+
then ex r being Element of REAL+ st
( u = r & [0,r] in X ) ;
hence u in REAL+ ; :: thesis: verum
end;
then reconsider X9 = { r where r is Element of REAL+ : [0,r] in X } as Subset of REAL+ ;
{ r where r is Element of REAL+ : [0,r] in Y } c= REAL+
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { r where r is Element of REAL+ : [0,r] in Y } or u in REAL+ )
assume u in { r where r is Element of REAL+ : [0,r] in Y } ; :: thesis: u in REAL+
then ex r being Element of REAL+ st
( u = r & [0,r] in Y ) ;
hence u in REAL+ ; :: thesis: verum
end;
then reconsider Y9 = { r where r is Element of REAL+ : [0,r] in Y } as Subset of REAL+ ;
consider e being object such that
A14: e in Y and
A15: e in [:{0},REAL+:] by A13, XBOOLE_0:3;
consider u, y1 being object such that
A16: u in {0} and
A17: y1 in REAL+ and
A18: e = [u,y1] by A15, ZFMISC_1:84;
reconsider y1 = y1 as Element of REAL+ by A17;
e in REAL by A14;
then A19: [0,y1] in REAL by A16, A18, TARSKI:def 1;
then reconsider y0 = [0,y1] as Real ;
A20: y0 in Y by A14, A16, A18, TARSKI:def 1;
then A21: y1 in Y9 ;
A22: y0 in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
A23: X c= [:{0},REAL+:]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in X or u in [:{0},REAL+:] )
assume A24: u in X ; :: thesis: u in [:{0},REAL+:]
then reconsider x = u as Real ;
hence u in [:{0},REAL+:] by A6, A24, XBOOLE_0:def 3; :: thesis: verum
end;
then consider e, x3 being object such that
A26: e in {0} and
A27: x3 in REAL+ and
A28: x1 = [e,x3] by A5, ZFMISC_1:84;
reconsider x3 = x3 as Element of REAL+ by A27;
x1 = [0,x3] by A26, A28, TARSKI:def 1;
then A29: x3 in X9 by A5;
for y9, x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds
y9 <=' x9
proof
let y9, x9 be Element of REAL+ ; :: thesis: ( y9 in Y9 & x9 in X9 implies y9 <=' x9 )
assume y9 in Y9 ; :: thesis: ( not x9 in X9 or y9 <=' x9 )
then A30: ex r1 being Element of REAL+ st
( y9 = r1 & [0,r1] in Y ) ;
assume x9 in X9 ; :: thesis: y9 <=' x9
then A31: ex r2 being Element of REAL+ st
( x9 = r2 & [0,r2] in X ) ;
then reconsider x = [0,x9], y = [0,y9] as Real by A30;
A32: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) by Lm4, ZFMISC_1:87;
x <= y by A1, A30, A31;
then consider x99, y99 being Element of REAL+ such that
A33: x = [0,x99] and
A34: ( y = [0,y99] & y99 <=' x99 ) by A32, XXREAL_0:def 5;
x9 = x99 by A33, XTUPLE_0:1;
hence y9 <=' x9 by A34, XTUPLE_0:1; :: thesis: verum
end;
then consider z9 being Element of REAL+ such that
A35: for y9, x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds
( y9 <=' z9 & z9 <=' x9 ) by A29, ARYTM_2:8;
A36: y1 <> 0 by A19, ARYTM_0:3;
y1 <=' z9 by A21, A29, A35;
then [0,z9] in REAL by A36, ARYTM_0:2, ARYTM_1:5;
then reconsider z = [0,z9] as Real ;
take z ; :: thesis: for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
let x, y be Real; :: thesis: ( x in X & y in Y implies ( x <= z & z <= y ) )
assume that
A37: x in X and
A38: y in Y ; :: thesis: ( x <= z & z <= y )
consider e, x9 being object such that
A39: e in {0} and
A40: x9 in REAL+ and
A41: x = [e,x9] by A23, A37, ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A40;
A42: z in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
A43: x = [0,x9] by A39, A41, TARSKI:def 1;
then A44: x9 in X9 by A37;
per cases ( y in REAL+ or y in [:{0},REAL+:] ) by A7, A38, XBOOLE_0:def 3;
suppose A47: y in [:{0},REAL+:] ; :: thesis: ( x <= z & z <= y )
then consider e, y9 being object such that
A48: e in {0} and
A49: y9 in REAL+ and
A50: y = [e,y9] by ZFMISC_1:84;
reconsider y9 = y9 as Element of REAL+ by A49;
A51: y = [0,y9] by A48, A50, TARSKI:def 1;
then y9 in Y9 by A38;
then ( y9 <=' z9 & z9 <=' x9 ) by A35, A44;
hence ( x <= z & z <= y ) by A23, A42, A37, A43, A47, A51, Lm1; :: thesis: verum
end;
end;
end;
suppose A52: X meets REAL+ ; :: thesis: ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
reconsider X9 = X /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
consider x1 being object such that
A53: x1 in X and
A54: x1 in REAL+ by A52, XBOOLE_0:3;
reconsider x1 = x1 as Element of REAL+ by A54;
x1 in REAL+ ;
then reconsider x0 = x1 as Real by ARYTM_0:1;
A55: Y c= REAL+
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Y or u in REAL+ )
assume A56: u in Y ; :: thesis: u in REAL+
then reconsider y = u as Real ;
hence u in REAL+ by A7, A56, XBOOLE_0:def 3; :: thesis: verum
end;
then reconsider Y9 = Y as Subset of REAL+ ;
for x9, y9 being Element of REAL+ st x9 in X9 & y9 in Y9 holds
x9 <=' y9
proof
let x9, y9 be Element of REAL+ ; :: thesis: ( x9 in X9 & y9 in Y9 implies x9 <=' y9 )
A58: X9 c= X by XBOOLE_1:17;
( x9 in REAL+ & y9 in REAL+ ) ;
then reconsider x = x9, y = y9 as Real by ARYTM_0:1;
assume ( x9 in X9 & y9 in Y9 ) ; :: thesis: x9 <=' y9
then x <= y by A1, A58;
then ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) by XXREAL_0:def 5;
hence x9 <=' y9 ; :: thesis: verum
end;
then consider z9 being Element of REAL+ such that
A59: for x9, y9 being Element of REAL+ st x9 in X9 & y9 in Y9 holds
( x9 <=' z9 & z9 <=' y9 ) by A8, ARYTM_2:8;
z9 in REAL+ ;
then reconsider z = z9 as Real by ARYTM_0:1;
take z ; :: thesis: for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )
let x, y be Real; :: thesis: ( x in X & y in Y implies ( x <= z & z <= y ) )
assume that
A60: x in X and
A61: y in Y ; :: thesis: ( x <= z & z <= y )
reconsider y9 = y as Element of REAL+ by A55, A61;
A62: x0 in X9 by A53, XBOOLE_0:def 4;
end;
end;
end;
end;
end;