let X, Y be Subset of REAL ; :: thesis: ( ( 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
; :: thesis: 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
;
:: thesis: 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:10;
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:10;
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 )
:: thesis: 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+ :]
;
:: thesis: 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 X' =
{ 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 Y' =
{ 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:103;
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 Y'
;
A22:
y0 in [:{0 },REAL+ :]
by Lm4, ZFMISC_1:106;
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:103;
reconsider x3 =
x3 as
Element of
REAL+ by A27;
x1 = [0 ,x3]
by A26, A28, TARSKI:def 1;
then A29:
x3 in X'
by A5;
for
y',
x' being
Element of
REAL+ st
y' in Y' &
x' in X' holds
y' <=' x'
proof
let y',
x' be
Element of
REAL+ ;
:: thesis: ( y' in Y' & x' in X' implies y' <=' x' )
assume
y' in Y'
;
:: thesis: ( not x' in X' or y' <=' x' )
then A30:
ex
r1 being
Element of
REAL+ st
(
y' = r1 &
[0 ,r1] in Y )
;
assume
x' in X'
;
:: thesis: y' <=' x'
then A31:
ex
r2 being
Element of
REAL+ st
(
x' = r2 &
[0 ,r2] in X )
;
then reconsider x =
[0 ,x'],
y =
[0 ,y'] as
real number by A30, XREAL_0:def 1;
A32:
(
x in [:{0 },REAL+ :] &
y in [:{0 },REAL+ :] )
by Lm4, ZFMISC_1:106;
x <= y
by A1, A30, A31;
then consider x'',
y'' being
Element of
REAL+ such that A33:
x = [0 ,x'']
and A34:
(
y = [0 ,y''] &
y'' <=' x'' )
by A32, XXREAL_0:def 5;
x' = x''
by A33, ZFMISC_1:33;
hence
y' <=' x'
by A34, ZFMISC_1:33;
:: thesis: verum
end; then consider z' being
Element of
REAL+ such that A35:
for
y',
x' being
Element of
REAL+ st
y' in Y' &
x' in X' holds
(
y' <=' z' &
z' <=' x' )
by A29, ARYTM_2:9;
A36:
y1 <> 0
by A19, ARYTM_0:3;
y1 <=' z'
by A21, A29, A35;
then
[0 ,z'] in REAL
by A36, ARYTM_0:2, ARYTM_1:5;
then reconsider z =
[0 ,z'] as
real number by XREAL_0:def 1;
take
z
;
:: thesis: for x, y being real number st x in X & y in Y holds
( x <= z & z <= y )let x,
y be
real number ;
:: 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,
x' being
set such that A39:
e in {0 }
and A40:
x' in REAL+
and A41:
x = [e,x']
by A23, A37, ZFMISC_1:103;
reconsider x' =
x' as
Element of
REAL+ by A40;
A42:
z in [:{0 },REAL+ :]
by Lm4, ZFMISC_1:106;
A43:
x = [0 ,x']
by A39, A41, TARSKI:def 1;
then A44:
x' in X'
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+
;
:: thesis: ( x <= z & z <= y )
z' <=' x'
by A21, A35, A44;
hence
x <= z
by A23, A42, A37, A43, Lm1;
:: thesis: 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;
:: thesis: verum end; suppose A47:
y in [:{0 },REAL+ :]
;
:: thesis: ( x <= z & z <= y )then consider e,
y' being
set such that A48:
e in {0 }
and A49:
y' in REAL+
and A50:
y = [e,y']
by ZFMISC_1:103;
reconsider y' =
y' as
Element of
REAL+ by A49;
A51:
y = [0 ,y']
by A48, A50, TARSKI:def 1;
then
y' in Y'
by A38;
then
(
y' <=' z' &
z' <=' x' )
by A35, A44;
hence
(
x <= z &
z <= y )
by A23, A42, A37, A43, A47, A51, Lm1;
:: thesis: verum end; hence
(
x <= z &
z <= y )
;
:: thesis: verum end; suppose A52:
X meets REAL+
;
:: thesis: 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 X' =
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 Y' =
Y as
Subset of
REAL+ ;
for
x',
y' being
Element of
REAL+ st
x' in X' &
y' in Y' holds
x' <=' y'
then consider z' being
Element of
REAL+ such that A59:
for
x',
y' being
Element of
REAL+ st
x' in X' &
y' in Y' holds
(
x' <=' z' &
z' <=' y' )
by A8, ARYTM_2:9;
z' in REAL+
;
then reconsider z =
z' as
real number by ARYTM_0:1, XREAL_0:def 1;
take
z
;
:: thesis: for x, y being real number st x in X & y in Y holds
( x <= z & z <= y )let x,
y be
real number ;
:: 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 y' =
y as
Element of
REAL+ by A55, A61;
A62:
x0 in X'
by A53, XBOOLE_0:def 4;
hence
(
x <= z &
z <= y )
;
:: thesis: verum end;
end; end;