let X, Y be Subset of REAL; ( ( for x, y being real number st x in X & y in Y holds
x <= y ) implies ex z being real number st
for x, y being real number st x in X & y in Y holds
( x <= z & z <= y ) )
assume A1:
for x, y being real number st x in X & y in Y holds
x <= y
; ex z being real number st
for x, y being real number 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 that A3:
X <> 0
and A4:
Y <> 0
;
ex z being real number st
for x, y being real number 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 number st
for
x,
y being
real number st
x in X &
y in Y holds
(
x <= z &
z <= y )
verumproof
per cases
( ( X misses REAL+ & Y misses [:{0},REAL+:] ) or Y meets [:{0},REAL+:] or X meets REAL+ )
;
suppose A13:
Y meets [:{0},REAL+:]
;
ex z being real number st
for x, y being real number 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+
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+
then reconsider Y9 =
{ r where r is Element of REAL+ : [0,r] in Y } as
Subset of
REAL+ ;
consider e being
set such that A14:
e in Y
and A15:
e in [:{0},REAL+:]
by A13, XBOOLE_0:3;
consider u,
y1 being
set 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 number by XREAL_0:def 1;
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+:]
then consider e,
x3 being
set 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+ ;
( y9 in Y9 & x9 in X9 implies y9 <=' x9 )
assume
y9 in Y9
;
( 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
;
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 number by A30, XREAL_0:def 1;
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, ZFMISC_1:27;
hence
y9 <=' x9
by A34, ZFMISC_1:27;
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 number by XREAL_0:def 1;
take
z
;
for x, y being real number st x in X & y in Y holds
( x <= z & z <= y )let x,
y be
real number ;
( x in X & y in Y implies ( x <= z & z <= y ) )assume that A37:
x in X
and A38:
y in Y
;
( x <= z & z <= y )consider e,
x9 being
set 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;
now per cases
( y in REAL+ or y in [:{0},REAL+:] )
by A7, A38, XBOOLE_0:def 3;
suppose A45:
y in REAL+
;
( x <= z & z <= y )
z9 <=' x9
by A21, A35, A44;
hence
x <= z
by A23, A42, A37, A43, Lm1;
z <= yA46:
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;
verum end; suppose A47:
y in [:{0},REAL+:]
;
( x <= z & z <= y )then consider e,
y9 being
set 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;
verum end; hence
(
x <= z &
z <= y )
;
verum end; suppose A52:
X meets REAL+
;
ex z being real number st
for x, y being real number 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
set 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 number by ARYTM_0:1, XREAL_0:def 1;
A55:
Y c= REAL+
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
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 number by ARYTM_0:1, XREAL_0:def 1;
take
z
;
for x, y being real number st x in X & y in Y holds
( x <= z & z <= y )let x,
y be
real number ;
( x in X & y in Y implies ( x <= z & z <= y ) )assume that A60:
x in X
and A61:
y in Y
;
( x <= z & z <= y )reconsider y9 =
y as
Element of
REAL+ by A55, A61;
A62:
x0 in X9
by A53, XBOOLE_0:def 4;
hence
(
x <= z &
z <= y )
;
verum end;
end; end;