begin
definition
let x,
y be
ext-real number ;
consistency
( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) )
by ARYTM_0:5, XBOOLE_0:3;
reflexivity
for x being ext-real number holds
( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )
connectedness
for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
end;
::
deftheorem Def5 defines
<= XXREAL_0:def 5 :
for x, y being ext-real number holds
( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( x <= y iff ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty ) ) ) );
Lm1:
+infty <> [0,0]
Lm2:
not +infty in REAL+
by ARYTM_0:1, ORDINAL1:5;
Lm3:
not -infty in REAL+
Lm4:
not +infty in [:{0},REAL+:]
Lm5:
not -infty in [:{0},REAL+:]
Lm6:
-infty < +infty
Lm7:
for a being ext-real number st -infty >= a holds
a = -infty
Lm8:
for a being ext-real number st +infty <= a holds
a = +infty
Lm9:
for a being ext-real number holds
( a in REAL or a = +infty or a = -infty )
begin
begin
theorem
for
a,
b,
c being
ext-real number holds
max (
(max ((min (a,b)),(min (b,c)))),
(min (c,a)))
= min (
(min ((max (a,b)),(max (b,c)))),
(max (c,a)))
begin