let X, Y be Subset of REAL; :: thesis:
assume A1: for x, y being Real st x in X & y in Y holds
x <= y ; :: thesis:

suppose A2: ( X = 0 or Y = 0 ) ; :: thesis:

take 1 ; :: thesis:
thus for x, y being Real st x in X & y in Y holds
( x <= 1 & 1 <= y ) by A2; :: thesis:

end;

suppose that A3: X <> 0 and
A4: Y <> 0 ; :: thesis:

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:

proof

per cases ;

suppose that A9: X misses REAL+ and
A10: Y misses [:{0},REAL+:] ; :: thesis:

take z = 0 ; :: thesis:
let x, y be Real; :: thesis:
assume that
A11: x in X and
A12: y in Y ; :: thesis:
( 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:
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:

end;

suppose A13: Y meets [:{0},REAL+:] ; :: thesis:

{ r where r is Element of REAL+ : [0,r] in X } c= REAL+

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in { r where r is Element of REAL+ : [0,r] in X } ; :: thesis:
then ex r being Element of REAL+ st
( u = r & [0,r] in X ) ;
hence u in REAL+ ; :: thesis:

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:
assume u in { r where r is Element of REAL+ : [0,r] in Y } ; :: thesis:
then ex r being Element of REAL+ st
( u = r & [0,r] in Y ) ;
hence u in REAL+ ; :: thesis:

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:
assume A24: u in X ; :: thesis:
then reconsider x = u as Real ;

now :: thesis:

assume x in REAL+ ; :: thesis:
then A25: not x in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
( x <= y0 & not y0 in REAL+ ) by A1, A22, A20, A24, ARYTM_0:5, XBOOLE_0:3;
hence contradiction by A25, XXREAL_0:def 5; :: thesis:

end;

hence u in [:{0},REAL+:] by A6, A24, XBOOLE_0:def 3; :: thesis:

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:
assume y9 in Y9 ; :: thesis:
then A30: ex r1 being Element of REAL+ st
( y9 = r1 & [0,r1] in Y ) ;
assume x9 in X9 ; :: thesis:
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:

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:
let x, y be Real; :: thesis:
assume that
A37: x in X and
A38: y in Y ; :: thesis:
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 by A7, A38, XBOOLE_0:def 3;

suppose A45: y in REAL+ ; :: thesis:

z9 <=' x9 by A21, A35, A44;
hence x <= z by A23, A42, A37, A43, Lm1; :: thesis:
A46: not y in [:{0},REAL+:] by A45, ARYTM_0:5, XBOOLE_0:3;
not z in REAL+ by A42, ARYTM_0:5, XBOOLE_0:3;
hence z <= y by A46, XXREAL_0:def 5; :: thesis:

end;

suppose A47: y in [:{0},REAL+:] ; :: thesis:

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:

end;

suppose A52: X meets REAL+ ; :: thesis:

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:
assume A56: u in Y ; :: thesis:
then reconsider y = u as Real ;

now :: thesis:

assume y in [:{0},REAL+:] ; :: thesis:
then A57: not y in REAL+ by ARYTM_0:5, XBOOLE_0:3;
( x0 <= y & not x0 in [:{0},REAL+:] ) by A1, A53, A56, ARYTM_0:5, XBOOLE_0:3;
hence contradiction by A57, XXREAL_0:def 5; :: thesis:

end;

hence u in REAL+ by A7, A56, XBOOLE_0:def 3; :: thesis:

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:
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:
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:

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:
let x, y be Real; :: thesis:
assume that
A60: x in X and
A61: y in Y ; :: thesis:
reconsider y9 = y as Element of REAL+ by A55, A61;
A62: x0 in X9 by A53, XBOOLE_0:def 4;

per cases by A6, A60, XBOOLE_0:def 3;

suppose x in REAL+ ; :: thesis:

then reconsider x9 = x as Element of REAL+ ;
x9 in X9 by A60, XBOOLE_0:def 4;
then ( x9 <=' z9 & z9 <=' y9 ) by A59, A61;
hence ( x <= z & z <= y ) by Lm1; :: thesis:

end;

suppose A63: x in [:{0},REAL+:] ; :: thesis:

A64: not z in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
not x in REAL+ by A63, ARYTM_0:5, XBOOLE_0:3;
hence x <= z by A64, XXREAL_0:def 5; :: thesis:
z9 <=' y9 by A62, A59, A61;
hence z <= y by Lm1; :: thesis:

end;