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;
consider x2 being
Element of
REAL such that A6:
x2 in Y
by A4, SUBSET_1:10;
A7:
X c= REAL+ \/ [:{0 },REAL+ :]
by NUMBERS:def 1, XBOOLE_1:1;
A8:
Y c= REAL+ \/ [:{0 },REAL+ :]
by NUMBERS:def 1, XBOOLE_1:1;
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 that A9:
X misses REAL+
and A10:
Y misses [:{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 )A11:
Y c= REAL+
by A8, A10, XBOOLE_1:73;
take z =
0 ;
:: 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 A12:
x in X
and A13:
y in Y
;
:: thesis: ( x <= z & z <= y )
( not
z in [:{0 },REAL+ :] & not
x in REAL+ )
by A9, A12, ARYTM_0:5, ARYTM_2:21, XBOOLE_0:3;
hence
x <= z
by XXREAL_0:def 5;
:: thesis: z <= yreconsider y' =
y as
Element of
REAL+ by A11, A13;
o <=' y'
by ARYTM_1:6;
hence
z <= y
by Lm1;
:: thesis: verum end; suppose
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 )then consider e being
set such that A14:
e in Y
and A15:
e in [:{0 },REAL+ :]
by 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;
{ 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+ ;
A20:
y0 in [:{0 },REAL+ :]
by Lm4, ZFMISC_1:106;
A21:
y0 in Y
by A14, A16, A18, TARSKI:def 1;
then A22:
y1 in Y'
;
A23:
X c= [:{0 },REAL+ :]
then consider e,
x3 being
set such that A27:
e in {0 }
and A28:
x3 in REAL+
and A29:
x1 = [e,x3]
by A5, ZFMISC_1:103;
reconsider x3 =
x3 as
Element of
REAL+ by A28;
A30:
x1 = [0 ,x3]
by A27, A29, TARSKI:def 1;
{ 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+ ;
A31:
x3 in X'
by A5, A30;
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 consider r1 being
Element of
REAL+ such that A32:
y' = r1
and A33:
[0 ,r1] in Y
;
assume
x' in X'
;
:: thesis: y' <=' x'
then consider r2 being
Element of
REAL+ such that A34:
x' = r2
and A35:
[0 ,r2] in X
;
reconsider x =
[0 ,x'],
y =
[0 ,y'] as
real number by A32, A33, A34, A35, XREAL_0:def 1;
A36:
(
x in [:{0 },REAL+ :] &
y in [:{0 },REAL+ :] )
by Lm4, ZFMISC_1:106;
x <= y
by A1, A32, A33, A34, A35;
then consider x'',
y'' being
Element of
REAL+ such that A37:
x = [0 ,x'']
and A38:
y = [0 ,y'']
and A39:
y'' <=' x''
by A36, XXREAL_0:def 5;
(
x' = x'' &
y' = y'' )
by A37, A38, ZFMISC_1:33;
hence
y' <=' x'
by A39;
:: thesis: verum
end; then consider z' being
Element of
REAL+ such that A40:
for
y',
x' being
Element of
REAL+ st
y' in Y' &
x' in X' holds
(
y' <=' z' &
z' <=' x' )
by A22, A31, ARYTM_2:9;
A41:
y1 <> 0
by A19, ARYTM_0:3;
y1 <=' z'
by A22, A31, A40;
then
[0 ,z'] in REAL
by A41, 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 )A42:
z in [:{0 },REAL+ :]
by Lm4, ZFMISC_1:106;
let x,
y be
real number ;
:: thesis: ( x in X & y in Y implies ( x <= z & z <= y ) )assume that A43:
x in X
and A44:
y in Y
;
:: thesis: ( x <= z & z <= y )consider e,
x' being
set such that A45:
e in {0 }
and A46:
x' in REAL+
and A47:
x = [e,x']
by A23, A43, ZFMISC_1:103;
reconsider x' =
x' as
Element of
REAL+ by A46;
A48:
x = [0 ,x']
by A45, A47, TARSKI:def 1;
then A49:
x' in X'
by A43;
now per cases
( y in REAL+ or y in [:{0 },REAL+ :] )
by A8, A44, XBOOLE_0:def 3;
suppose A50:
y in REAL+
;
:: thesis: ( x <= z & z <= y )
(
y1 <=' z' &
z' <=' x' )
by A22, A40, A49;
hence
x <= z
by A23, A42, A43, A48, Lm1;
:: thesis: z <= y
( not
z in REAL+ & not
y in [:{0 },REAL+ :] )
by A42, A50, ARYTM_0:5, XBOOLE_0:3;
hence
z <= y
by XXREAL_0:def 5;
:: thesis: verum suppose A51:
y in [:{0 },REAL+ :]
;
:: thesis: ( x <= z & z <= y )then consider e,
y' being
set such that A52:
e in {0 }
and A53:
y' in REAL+
and A54:
y = [e,y']
by ZFMISC_1:103;
reconsider y' =
y' as
Element of
REAL+ by A53;
A55:
y = [0 ,y']
by A52, A54, TARSKI:def 1;
then
y' in Y'
by A44;
then
(
y' <=' z' &
z' <=' x' )
by A40, A49;
hence
(
x <= z &
z <= y )
by A23, A42, A43, A48, A51, A55, Lm1;
:: thesis: verum end; hence
(
x <= z &
z <= y )
;
:: thesis: verum end; suppose
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 )then consider x1 being
set such that A56:
x1 in X
and A57:
x1 in REAL+
by XBOOLE_0:3;
reconsider x1 =
x1 as
Element of
REAL+ by A57;
x1 in REAL+
;
then reconsider x0 =
x1 as
real number by ARYTM_0:1, XREAL_0:def 1;
reconsider X' =
X /\ REAL+ as
Subset of
REAL+ by XBOOLE_1:17;
A58:
x0 in X'
by A56, XBOOLE_0:def 4;
A59:
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 A64:
for
x',
y' being
Element of
REAL+ st
x' in X' &
y' in Y' holds
(
x' <=' z' &
z' <=' y' )
by A6, A58, 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 A65:
x in X
and A66:
y in Y
;
:: thesis: ( x <= z & z <= y )reconsider y' =
y as
Element of
REAL+ by A59, A66;
hence
(
x <= z &
z <= y )
;
:: thesis: verum end;
end; end;