:: XXREAL_2 semantic presentation

begin

scheme :: XXREAL_2:sch 1
FinInter{ F1() ->  Integer, F2() ->  Integer, F3( set ) ->  set , P1[ set ] } :
  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  is finite
proof
set F =  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  ;
percases ( F2() < F1() or F1() <= F2() ) ;
supposeA1: F2() < F1() ; ::_thesis:  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  is finite
now__::_thesis:_not__{__F3(i)_where_i_is_Element_of_INT_:_(_F1()_<=_i_&_i_<=_F2()_&_P1[i]_)__}__<>_{}
assume   {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  by XBOOLE_0:def_1;
 ex i being Element of INT st
( x = F3(i) & F1() <= i & i <= F2() & P1[i] ) by A2;
hence  contradiction by A1, XXREAL_0:2; ::_thesis: verum
end;
then reconsider F =  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  as empty set ;
 F is finite ;
hence   {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  is finite ; ::_thesis: verum
end;
suppose F1() <= F2() ; ::_thesis:  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  is finite
then reconsider k = F2() - F1() as Element of NAT by INT_1:5;
set F =  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  ;
defpred S1[ set , set ] means  ex i being Integer st
( $1 = i & $2 = F3((i + F1())) );
A3: for e being set st e in k + 1 holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in k + 1 implies ex u being set st S1[e,u] )
assume  e in k + 1 ; ::_thesis: ex u being set st S1[e,u]
then reconsider i = e as Nat ;
take  F3((i + F1())) ; ::_thesis: S1[e,F3((i + F1()))]
take  i ; ::_thesis: ( e = i & F3((i + F1())) = F3((i + F1())) )
thus  ( e = i & F3((i + F1())) = F3((i + F1())) ) ; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = k + 1 and
A5: for i being set st i in k + 1 holds
S1[i,f . i] from CLASSES1:sch_1(A3);
A6:  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  or x in rng f )
assume  x in  {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  ; ::_thesis: x in rng f
then consider j being Element of INT  such that
A7: x = F3(j) and
A8: F1() <= j and
A9: j <= F2() and
 P1[j] ;
reconsider l = j - F1() as Element of NAT by A8, INT_1:5;
 l <= k by A9, XREAL_1:9;
then  l < k + 1 by NAT_1:13;
then A10: l in k + 1 by NAT_1:44;
then  S1[j - F1(),f . (j - F1())] by A5;
then f . (j - F1()) = F3(((j + F1()) - F1()))
.= F3(j) ;
hence  x in rng f by A4, A7, A10, FUNCT_1:def_3; ::_thesis: verum
end;
 rng f is finite by A4, FINSET_1:8;
hence   {  F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] )  }  is finite by A6; ::_thesis: verum
end;
end;
end;


definition
let X be ext-real-membered set ;
mode UpperBound of X ->  ext-real number  means :Def1: :: XXREAL_2:def 1
 for x being ext-real number st x in X holds
x <= it;
existence
 ex b1 being ext-real number st
for x being ext-real number st x in X holds
x <= b1
proof
take  +infty ; ::_thesis: for x being ext-real number st x in X holds
x <= +infty
thus  for x being ext-real number st x in X holds
x <= +infty by XXREAL_0:4; ::_thesis: verum
end;
mode LowerBound of X ->  ext-real number  means :Def2: :: XXREAL_2:def 2
 for x being ext-real number st x in X holds
it <= x;
existence
 ex b1 being ext-real number st
for x being ext-real number st x in X holds
b1 <= x
proof
take  -infty ; ::_thesis: for x being ext-real number st x in X holds
-infty <= x
thus  for x being ext-real number st x in X holds
-infty <= x by XXREAL_0:5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines UpperBound XXREAL_2:def_1_:_
 for X being ext-real-membered set
for b2 being ext-real number holds
( b2 is UpperBound of X iff for x being ext-real number st x in X holds
x <= b2 );

:: deftheorem Def2 defines LowerBound XXREAL_2:def_2_:_
 for X being ext-real-membered set
for b2 being ext-real number holds
( b2 is LowerBound of X iff for x being ext-real number st x in X holds
b2 <= x );

definition
let X be ext-real-membered set ;
func sup X ->  ext-real number  means :Def3: :: XXREAL_2:def 3
( it is UpperBound of X & ( for x being UpperBound of X holds it <= x ) );
existence
 ex b1 being ext-real number st
( b1 is UpperBound of X & ( for x being UpperBound of X holds b1 <= x ) )
proof
defpred S1[ set ] means $1 is UpperBound of X;
defpred S2[ set ] means $1 in X;
A1: for r, s being ext-real number st S2[r] & S1[s] holds
r <= s by Def1;
consider s being ext-real number  such that
A2: for r being ext-real number st S2[r] holds
r <= s and
A3: for r being ext-real number st S1[r] holds
s <= r from XXREAL_1:sch_1(A1);
take  s ; ::_thesis: ( s is UpperBound of X & ( for x being UpperBound of X holds s <= x ) )
thus  s is UpperBound of X by A2, Def1; ::_thesis: for x being UpperBound of X holds s <= x
thus  for x being UpperBound of X holds s <= x by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ext-real number st b1 is UpperBound of X & ( for x being UpperBound of X holds b1 <= x ) & b2 is UpperBound of X & ( for x being UpperBound of X holds b2 <= x ) holds
b1 = b2
proof
let y, z be ext-real number ; ::_thesis: ( y is UpperBound of X & ( for x being UpperBound of X holds y <= x ) & z is UpperBound of X & ( for x being UpperBound of X holds z <= x ) implies y = z )
assume that
A4: y is UpperBound of X and
A5: for x being UpperBound of X holds y <= x and
A6: z is UpperBound of X and
A7: for x being UpperBound of X holds z <= x ; ::_thesis: y = z
A8: y <= z by A5, A6;
 z <= y by A4, A7;
hence  y = z by A8, XXREAL_0:1; ::_thesis: verum
end;
func inf X ->  ext-real number  means :Def4: :: XXREAL_2:def 4
( it is LowerBound of X & ( for x being LowerBound of X holds x <= it ) );
existence
 ex b1 being ext-real number st
( b1 is LowerBound of X & ( for x being LowerBound of X holds x <= b1 ) )
proof
defpred S1[ set ] means $1 in X;
defpred S2[ set ] means $1 is LowerBound of X;
A9: for r, s being ext-real number st S2[r] & S1[s] holds
r <= s by Def2;
consider s being ext-real number  such that
A10: for r being ext-real number st S2[r] holds
r <= s and
A11: for r being ext-real number st S1[r] holds
s <= r from XXREAL_1:sch_1(A9);
take  s ; ::_thesis: ( s is LowerBound of X & ( for x being LowerBound of X holds x <= s ) )
thus  s is LowerBound of X by A11, Def2; ::_thesis: for x being LowerBound of X holds x <= s
thus  for x being LowerBound of X holds x <= s by A10; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ext-real number st b1 is LowerBound of X & ( for x being LowerBound of X holds x <= b1 ) & b2 is LowerBound of X & ( for x being LowerBound of X holds x <= b2 ) holds
b1 = b2
proof
let y, z be ext-real number ; ::_thesis: ( y is LowerBound of X & ( for x being LowerBound of X holds x <= y ) & z is LowerBound of X & ( for x being LowerBound of X holds x <= z ) implies y = z )
assume that
A12: y is LowerBound of X and
A13: for x being LowerBound of X holds x <= y and
A14: z is LowerBound of X and
A15: for x being LowerBound of X holds x <= z ; ::_thesis: y = z
A16: z <= y by A13, A14;
 y <= z by A12, A15;
hence  y = z by A16, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines sup XXREAL_2:def_3_:_
 for X being ext-real-membered set
for b2 being ext-real number holds
( b2 = sup X iff ( b2 is UpperBound of X & ( for x being UpperBound of X holds b2 <= x ) ) );

:: deftheorem Def4 defines inf XXREAL_2:def_4_:_
 for X being ext-real-membered set
for b2 being ext-real number holds
( b2 = inf X iff ( b2 is LowerBound of X & ( for x being LowerBound of X holds x <= b2 ) ) );

definition
let X be ext-real-membered set ;
attrX is left_end  means :Def5: :: XXREAL_2:def 5
 inf X in X;
attrX is right_end  means :Def6: :: XXREAL_2:def 6
 sup X in X;
end;

:: deftheorem Def5 defines left_end XXREAL_2:def_5_:_
 for X being ext-real-membered set holds
( X is left_end iff inf X in X );

:: deftheorem Def6 defines right_end XXREAL_2:def_6_:_
 for X being ext-real-membered set holds
( X is right_end iff sup X in X );

theorem Th1: :: XXREAL_2:1
for y, x being ext-real number holds
( y is UpperBound of {x} iff x <= y )
proof
let y, x be ext-real number ; ::_thesis: ( y is UpperBound of {x} iff x <= y )
 x in {x} by TARSKI:def_1;
hence  ( y is UpperBound of {x} implies x <= y ) by Def1; ::_thesis: ( x <= y implies y is UpperBound of {x} )
assume A1: x <= y ; ::_thesis: y is UpperBound of {x}
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in {x} implies z <= y )
assume  z in {x} ; ::_thesis: z <= y
hence  z <= y by A1, TARSKI:def_1; ::_thesis: verum
end;

theorem Th2: :: XXREAL_2:2
for y, x being ext-real number holds
( y is LowerBound of {x} iff y <= x )
proof
let y, x be ext-real number ; ::_thesis: ( y is LowerBound of {x} iff y <= x )
 x in {x} by TARSKI:def_1;
hence  ( y is LowerBound of {x} implies y <= x ) by Def2; ::_thesis: ( y <= x implies y is LowerBound of {x} )
assume A1: y <= x ; ::_thesis: y is LowerBound of {x}
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in {x} implies y <= z )
assume  z in {x} ; ::_thesis: y <= z
hence  y <= z by A1, TARSKI:def_1; ::_thesis: verum
end;

Lm1:  for x being ext-real number holds sup {x} = x
proof
let x be ext-real number ; ::_thesis: sup {x} = x
A1: for z being UpperBound of {x} holds x <= z
proof
let z be UpperBound of {x}; ::_thesis: x <= z
 x in {x} by TARSKI:def_1;
hence  x <= z by Def1; ::_thesis: verum
end;
 x is UpperBound of {x} by Th1;
hence  sup {x} = x by A1, Def3; ::_thesis: verum
end;

Lm2:  for x being ext-real number holds inf {x} = x
proof
let x be ext-real number ; ::_thesis: inf {x} = x
A1: for z being LowerBound of {x} holds z <= x
proof
let z be LowerBound of {x}; ::_thesis: z <= x
 x in {x} by TARSKI:def_1;
hence  z <= x by Def2; ::_thesis: verum
end;
 x is LowerBound of {x} by Th2;
hence  inf {x} = x by A1, Def4; ::_thesis: verum
end;

registration
cluster  ->  ext-real-membered for Element of Fin ExtREAL;
coherence
 for b1 being Element of Fin ExtREAL holds b1 is ext-real-membered
proof
let X be Element of Fin ExtREAL; ::_thesis: X is ext-real-membered
 X c= ExtREAL by FINSUB_1:def_5;
hence  X is ext-real-membered ; ::_thesis: verum
end;
end;


theorem Th3: :: XXREAL_2:3
for x being ext-real number
for A being ext-real-membered set st x in A holds
inf A <= x
proof
let x be ext-real number ; ::_thesis: for A being ext-real-membered set st x in A holds
inf A <= x
let A be ext-real-membered set ; ::_thesis: ( x in A implies inf A <= x )
 inf A is LowerBound of A by Def4;
hence  ( x in A implies inf A <= x ) by Def2; ::_thesis: verum
end;

theorem Th4: :: XXREAL_2:4
for x being ext-real number
for A being ext-real-membered set st x in A holds
x <= sup A
proof
let x be ext-real number ; ::_thesis: for A being ext-real-membered set st x in A holds
x <= sup A
let A be ext-real-membered set ; ::_thesis: ( x in A implies x <= sup A )
 sup A is UpperBound of A by Def3;
hence  ( x in A implies x <= sup A ) by Def1; ::_thesis: verum
end;

theorem Th5: :: XXREAL_2:5
for B, A being ext-real-membered set st B c= A holds
for x being LowerBound of A holds x is LowerBound of B
proof
let B, A be ext-real-membered set ; ::_thesis: ( B c= A implies for x being LowerBound of A holds x is LowerBound of B )
assume A1: B c= A ; ::_thesis: for x being LowerBound of A holds x is LowerBound of B
let x be LowerBound of A; ::_thesis: x is LowerBound of B
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( y in B implies x <= y )
assume  y in B ; ::_thesis: x <= y
hence  x <= y by A1, Def2; ::_thesis: verum
end;

theorem Th6: :: XXREAL_2:6
for B, A being ext-real-membered set st B c= A holds
for x being UpperBound of A holds x is UpperBound of B
proof
let B, A be ext-real-membered set ; ::_thesis: ( B c= A implies for x being UpperBound of A holds x is UpperBound of B )
assume A1: B c= A ; ::_thesis: for x being UpperBound of A holds x is UpperBound of B
let x be UpperBound of A; ::_thesis: x is UpperBound of B
let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( y in B implies y <= x )
assume  y in B ; ::_thesis: y <= x
hence  y <= x by A1, Def1; ::_thesis: verum
end;

theorem Th7: :: XXREAL_2:7
for A, B being ext-real-membered set
for x being LowerBound of A
for y being LowerBound of B holds min (x,y) is LowerBound of A \/ B
proof
let A, B be ext-real-membered set ; ::_thesis: for x being LowerBound of A
for y being LowerBound of B holds min (x,y) is LowerBound of A \/ B
let x be LowerBound of A; ::_thesis: for y being LowerBound of B holds min (x,y) is LowerBound of A \/ B
let y be LowerBound of B; ::_thesis: min (x,y) is LowerBound of A \/ B
set m = min (x,y);
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in A \/ B implies min (x,y) <= z )
assume A1: z in A \/ B ; ::_thesis: min (x,y) <= z
percases ( z in A or z in B ) by A1, XBOOLE_0:def_3;
supposeA2: z in A ; ::_thesis: min (x,y) <= z
A3: min (x,y) <= x by XXREAL_0:17;
 x <= z by A2, Def2;
hence  min (x,y) <= z by A3, XXREAL_0:2; ::_thesis: verum
end;
supposeA4: z in B ; ::_thesis: min (x,y) <= z
A5: min (x,y) <= y by XXREAL_0:17;
 y <= z by A4, Def2;
hence  min (x,y) <= z by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th8: :: XXREAL_2:8
for A, B being ext-real-membered set
for x being UpperBound of A
for y being UpperBound of B holds max (x,y) is UpperBound of A \/ B
proof
let A, B be ext-real-membered set ; ::_thesis: for x being UpperBound of A
for y being UpperBound of B holds max (x,y) is UpperBound of A \/ B
let x be UpperBound of A; ::_thesis: for y being UpperBound of B holds max (x,y) is UpperBound of A \/ B
let y be UpperBound of B; ::_thesis: max (x,y) is UpperBound of A \/ B
set m = max (x,y);
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in A \/ B implies z <= max (x,y) )
assume A1: z in A \/ B ; ::_thesis: z <= max (x,y)
percases ( z in A or z in B ) by A1, XBOOLE_0:def_3;
supposeA2: z in A ; ::_thesis: z <= max (x,y)
A3: x <= max (x,y) by XXREAL_0:25;
 z <= x by A2, Def1;
hence  z <= max (x,y) by A3, XXREAL_0:2; ::_thesis: verum
end;
supposeA4: z in B ; ::_thesis: z <= max (x,y)
A5: y <= max (x,y) by XXREAL_0:25;
 z <= y by A4, Def1;
hence  z <= max (x,y) by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th9: :: XXREAL_2:9
for A, B being ext-real-membered set holds inf (A \/ B) = min ((inf A),(inf B))
proof
let A, B be ext-real-membered set ; ::_thesis: inf (A \/ B) = min ((inf A),(inf B))
set m = min ((inf A),(inf B));
A1: inf B is LowerBound of B by Def4;
A2: for x being LowerBound of A \/ B holds x <= min ((inf A),(inf B))
proof
let x be LowerBound of A \/ B; ::_thesis: x <= min ((inf A),(inf B))
 x is LowerBound of B by Th5, XBOOLE_1:7;
then A3: x <= inf B by Def4;
 x is LowerBound of A by Th5, XBOOLE_1:7;
then  x <= inf A by Def4;
hence  x <= min ((inf A),(inf B)) by A3, XXREAL_0:20; ::_thesis: verum
end;
 inf A is LowerBound of A by Def4;
then  min ((inf A),(inf B)) is LowerBound of A \/ B by A1, Th7;
hence  inf (A \/ B) = min ((inf A),(inf B)) by A2, Def4; ::_thesis: verum
end;

theorem Th10: :: XXREAL_2:10
for A, B being ext-real-membered set holds sup (A \/ B) = max ((sup A),(sup B))
proof
let A, B be ext-real-membered set ; ::_thesis: sup (A \/ B) = max ((sup A),(sup B))
set m = max ((sup A),(sup B));
A1: sup B is UpperBound of B by Def3;
A2: for x being UpperBound of A \/ B holds max ((sup A),(sup B)) <= x
proof
let x be UpperBound of A \/ B; ::_thesis: max ((sup A),(sup B)) <= x
 x is UpperBound of B by Th6, XBOOLE_1:7;
then A3: sup B <= x by Def3;
 x is UpperBound of A by Th6, XBOOLE_1:7;
then  sup A <= x by Def3;
hence  max ((sup A),(sup B)) <= x by A3, XXREAL_0:28; ::_thesis: verum
end;
 sup A is UpperBound of A by Def3;
then  max ((sup A),(sup B)) is UpperBound of A \/ B by A1, Th8;
hence  sup (A \/ B) = max ((sup A),(sup B)) by A2, Def3; ::_thesis: verum
end;

registration
cluster ext-real-membered non empty finite  ->  ext-real-membered non empty left_end right_end for set ;
coherence
 for b1 being ext-real-membered non empty set st b1 is finite holds
( b1 is left_end & b1 is right_end )
proof
let X be ext-real-membered non empty set ; ::_thesis: ( X is finite implies ( X is left_end & X is right_end ) )
defpred S1[ ext-real-membered non empty set ] means ( c1 is left_end & c1 is right_end );
assume A1: X is finite ; ::_thesis: ( X is left_end & X is right_end )
 X c= ExtREAL by MEMBERED:2;
then A2: X is non empty Element of Fin ExtREAL by A1, FINSUB_1:def_5;
A3: for B1, B2 being non empty Element of Fin ExtREAL st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin ExtREAL; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume A4: S1[B1] ; ::_thesis: ( not S1[B2] or S1[B1 \/ B2] )
 inf (B1 \/ B2) = min ((inf B1),(inf B2)) by Th9;
then A5: ( inf (B1 \/ B2) = inf B1 or inf (B1 \/ B2) = inf B2 ) by XXREAL_0:15;
assume A6: S1[B2] ; ::_thesis: S1[B1 \/ B2]
then A7: inf B2 in B2 by Def5;
 inf B1 in B1 by A4, Def5;
hence  inf (B1 \/ B2) in B1 \/ B2 by A7, A5, XBOOLE_0:def_3; :: according to XXREAL_2:def_5 ::_thesis: B1 \/ B2 is right_end
 sup (B1 \/ B2) = max ((sup B1),(sup B2)) by Th10;
then A8: ( sup (B1 \/ B2) = sup B1 or sup (B1 \/ B2) = sup B2 ) by XXREAL_0:16;
A9: sup B2 in B2 by A6, Def6;
 sup B1 in B1 by A4, Def6;
hence  sup (B1 \/ B2) in B1 \/ B2 by A9, A8, XBOOLE_0:def_3; :: according to XXREAL_2:def_6 ::_thesis: verum
end;
A10: for x being Element of ExtREAL holds S1[{.x.}]
proof
let x be Element of ExtREAL ; ::_thesis: S1[{.x.}]
 sup {x} = x by Lm1;
then A11: sup {x} in {x} by TARSKI:def_1;
 inf {x} = x by Lm2;
then  inf {x} in {x} by TARSKI:def_1;
hence  S1[{.x.}] by A11, Def5, Def6; ::_thesis: verum
end;
 for B being non empty Element of Fin ExtREAL holds S1[B] from SETWISEO:sch_3(A10, A3);
hence  ( X is left_end & X is right_end ) by A2; ::_thesis: verum
end;
end;

registration
cluster natural-membered non empty  ->  natural-membered non empty left_end for set ;
coherence
 for b1 being natural-membered non empty set holds b1 is left_end
proof
let X be natural-membered non empty set ; ::_thesis: X is left_end
defpred S1[ set ] means c1 in X;
A1: ex k being Nat st S1[k] by MEMBERED:12;
consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A1);
A4: k is LowerBound of X
proof
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( y in X implies k <= y )
assume  y in X ; ::_thesis: k <= y
hence  k <= y by A3; ::_thesis: verum
end;
 for x being LowerBound of X holds x <= k by A2, Def2;
hence  inf X in X by A2, A4, Def4; :: according to XXREAL_2:def_5 ::_thesis: verum
end;
end;

registration
cluster complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty left_end right_end for set ;
existence
 ex b1 being natural-membered non empty set st b1 is right_end
proof
take  {0} ; ::_thesis: {0} is right_end
thus  {0} is right_end ; ::_thesis: verum
end;
end;

notation
let X be ext-real-membered left_end set ;
synonym  min X for  inf X;
end;

notation
let X be ext-real-membered right_end set ;
synonym  max X for  sup X;
end;

definition
let X be ext-real-membered left_end set ;
redefine func inf X means :Def7: :: XXREAL_2:def 7
( it in X & ( for x being ext-real number st x in X holds
it <= x ) );
compatibility
 for b1 being ext-real number holds
( b1 = inf X iff ( b1 in X & ( for x being ext-real number st x in X holds
b1 <= x ) ) )
proof
let y be ext-real number ; ::_thesis: ( y = inf X iff ( y in X & ( for x being ext-real number st x in X holds
y <= x ) ) )
thus  ( y = min X implies ( y in X & ( for x being ext-real number st x in X holds
y <= x ) ) ) by Def5, Th3; ::_thesis: ( y in X & ( for x being ext-real number st x in X holds
y <= x ) implies y = inf X )
assume that
A1: y in X and
A2: for x being ext-real number st x in X holds
y <= x ; ::_thesis: y = inf X
A3: for x being LowerBound of X holds x <= y by A1, Def2;
 y is LowerBound of X by A2, Def2;
hence  y = inf X by A3, Def4; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines inf XXREAL_2:def_7_:_
 for X being ext-real-membered left_end set
for b2 being ext-real number holds
( b2 = inf X iff ( b2 in X & ( for x being ext-real number st x in X holds
b2 <= x ) ) );

definition
let X be ext-real-membered right_end set ;
redefine func sup X means :Def8: :: XXREAL_2:def 8
( it in X & ( for x being ext-real number st x in X holds
x <= it ) );
compatibility
 for b1 being ext-real number holds
( b1 = sup X iff ( b1 in X & ( for x being ext-real number st x in X holds
x <= b1 ) ) )
proof
let y be ext-real number ; ::_thesis: ( y = sup X iff ( y in X & ( for x being ext-real number st x in X holds
x <= y ) ) )
thus  ( y = max X implies ( y in X & ( for x being ext-real number st x in X holds
x <= y ) ) ) by Def6, Th4; ::_thesis: ( y in X & ( for x being ext-real number st x in X holds
x <= y ) implies y = sup X )
assume that
A1: y in X and
A2: for x being ext-real number st x in X holds
x <= y ; ::_thesis: y = sup X
A3: for x being UpperBound of X holds y <= x by A1, Def1;
 y is UpperBound of X by A2, Def1;
hence  y = sup X by A3, Def3; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines sup XXREAL_2:def_8_:_
 for X being ext-real-membered right_end set
for b2 being ext-real number holds
( b2 = sup X iff ( b2 in X & ( for x being ext-real number st x in X holds
x <= b2 ) ) );

theorem :: XXREAL_2:11
for x being ext-real number holds max {x} = x by Lm1;

Lm3:  for x, y being ext-real number st x <= y holds
y is UpperBound of {x,y}
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies y is UpperBound of {x,y} )
assume A1: x <= y ; ::_thesis: y is UpperBound of {x,y}
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in {x,y} implies z <= y )
assume  z in {x,y} ; ::_thesis: z <= y
hence  z <= y by A1, TARSKI:def_2; ::_thesis: verum
end;

Lm4:  for x, y being ext-real number
for z being UpperBound of {x,y} holds y <= z
proof
let x, y be ext-real number ; ::_thesis: for z being UpperBound of {x,y} holds y <= z
let z be UpperBound of {x,y}; ::_thesis: y <= z
 y in {x,y} by TARSKI:def_2;
hence  y <= z by Def1; ::_thesis: verum
end;

theorem :: XXREAL_2:12
for x, y being ext-real number holds max (x,y) = max {x,y}
proof
let x, y be ext-real number ; ::_thesis: max (x,y) = max {x,y}
now__::_thesis:_(_(_x_<=_y_&_max_{x,y}_=_y_)_or_(_y_<_x_&_max_{x,y}_=_x_)_)
percases ( x <= y or y < x ) ;
caseA1: x <= y ; ::_thesis: max {x,y} = y
A2: for z being UpperBound of {x,y} holds y <= z by Lm4;
 y is UpperBound of {x,y} by A1, Lm3;
hence  max {x,y} = y by A2, Def3; ::_thesis: verum
end;
caseA3: y < x ; ::_thesis: max {x,y} = x
A4: for z being UpperBound of {x,y} holds x <= z by Lm4;
 x is UpperBound of {x,y} by A3, Lm3;
hence  max {x,y} = x by A4, Def3; ::_thesis: verum
end;
end;
end;
hence  max (x,y) = max {x,y} by XXREAL_0:def_10; ::_thesis: verum
end;

theorem :: XXREAL_2:13
for x being ext-real number holds min {x} = x by Lm2;

Lm5:  for y, x being ext-real number st y <= x holds
y is LowerBound of {x,y}
proof
let y, x be ext-real number ; ::_thesis: ( y <= x implies y is LowerBound of {x,y} )
assume A1: y <= x ; ::_thesis: y is LowerBound of {x,y}
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in {x,y} implies y <= z )
assume  z in {x,y} ; ::_thesis: y <= z
hence  y <= z by A1, TARSKI:def_2; ::_thesis: verum
end;

Lm6:  for x, y being ext-real number
for z being LowerBound of {x,y} holds z <= y
proof
let x, y be ext-real number ; ::_thesis: for z being LowerBound of {x,y} holds z <= y
let z be LowerBound of {x,y}; ::_thesis: z <= y
 y in {x,y} by TARSKI:def_2;
hence  z <= y by Def2; ::_thesis: verum
end;

theorem :: XXREAL_2:14
for x, y being ext-real number holds min {x,y} = min (x,y)
proof
let x, y be ext-real number ; ::_thesis: min {x,y} = min (x,y)
now__::_thesis:_(_(_y_<=_x_&_min_{x,y}_=_y_)_or_(_x_<_y_&_min_{x,y}_=_x_)_)
percases ( y <= x or x < y ) ;
caseA1: y <= x ; ::_thesis: min {x,y} = y
A2: for z being LowerBound of {x,y} holds z <= y by Lm6;
 y is LowerBound of {x,y} by A1, Lm5;
hence  min {x,y} = y by A2, Def4; ::_thesis: verum
end;
caseA3: x < y ; ::_thesis: min {x,y} = x
A4: for z being LowerBound of {x,y} holds z <= x by Lm6;
 x is LowerBound of {x,y} by A3, Lm5;
hence  min {x,y} = x by A4, Def4; ::_thesis: verum
end;
end;
end;
hence  min {x,y} = min (x,y) by XXREAL_0:def_9; ::_thesis: verum
end;

definition
let X be ext-real-membered set ;
attrX is bounded_below  means :Def9: :: XXREAL_2:def 9
 ex r being real number st r is LowerBound of X;
attrX is bounded_above  means :Def10: :: XXREAL_2:def 10
 ex r being real number st r is UpperBound of X;
end;

:: deftheorem Def9 defines bounded_below XXREAL_2:def_9_:_
 for X being ext-real-membered set holds
( X is bounded_below iff ex r being real number st r is LowerBound of X );

:: deftheorem Def10 defines bounded_above XXREAL_2:def_10_:_
 for X being ext-real-membered set holds
( X is bounded_above iff ex r being real number st r is UpperBound of X );

registration
cluster natural-membered non empty finite for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is finite & b1 is natural-membered )
proof
take  {0} ; ::_thesis: ( not {0} is empty & {0} is finite & {0} is natural-membered )
thus  ( not {0} is empty & {0} is finite & {0} is natural-membered ) ; ::_thesis: verum
end;
end;

definition
let X be ext-real-membered set ;
attrX is real-bounded  means :Def11: :: XXREAL_2:def 11
( X is bounded_below & X is bounded_above );
end;

:: deftheorem Def11 defines real-bounded XXREAL_2:def_11_:_
 for X being ext-real-membered set holds
( X is real-bounded iff ( X is bounded_below & X is bounded_above ) );

registration
cluster ext-real-membered real-bounded  ->  ext-real-membered bounded_below bounded_above for set ;
coherence
 for b1 being ext-real-membered set st b1 is real-bounded holds
( b1 is bounded_above & b1 is bounded_below ) by Def11;
cluster ext-real-membered bounded_below bounded_above  ->  ext-real-membered real-bounded for set ;
coherence
 for b1 being ext-real-membered set st b1 is bounded_above & b1 is bounded_below holds
b1 is real-bounded by Def11;
end;

registration
cluster real-membered finite  ->  real-membered real-bounded for set ;
coherence
 for b1 being real-membered set st b1 is finite holds
b1 is real-bounded
proof
let X be real-membered set ; ::_thesis: ( X is finite implies X is real-bounded )
assume A1: X is finite ; ::_thesis: X is real-bounded
percases ( X is empty or not X is empty ) ;
supposeA2: X is empty ; ::_thesis: X is real-bounded
thus  X is bounded_below :: according to XXREAL_2:def_11 ::_thesis: X is bounded_above
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies 0 <= x )
thus  ( x in X implies 0 <= x ) by A2; ::_thesis: verum
end;
take  0 ; :: according to XXREAL_2:def_10 ::_thesis: 0 is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= 0 )
thus  ( x in X implies x <= 0 ) by A2; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: X is real-bounded
then reconsider Y = X as real-membered non empty finite set by A1;
 inf Y in X by Def5;
then reconsider m = inf X as real number ;
thus  X is bounded_below :: according to XXREAL_2:def_11 ::_thesis: X is bounded_above
proof
take  m ; :: according to XXREAL_2:def_9 ::_thesis: m is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies m <= x )
assume  x in X ; ::_thesis: m <= x
hence  m <= x by Th3; ::_thesis: verum
end;
 sup Y in X by Def6;
then reconsider m = sup X as real number ;
take  m ; :: according to XXREAL_2:def_10 ::_thesis: m is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= m )
assume  x in X ; ::_thesis: x <= m
hence  x <= m by Th4; ::_thesis: verum
end;
end;
end;
end;

registration
cluster complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty left_end real-bounded for set ;
existence
 ex b1 being natural-membered non empty set st b1 is real-bounded
proof
take  {0} ; ::_thesis: {0} is real-bounded
thus  {0} is real-bounded ; ::_thesis: verum
end;
end;

theorem Th15: :: XXREAL_2:15
for X being real-membered non empty set st X is bounded_below holds
inf X in REAL
proof
let X be real-membered non empty set ; ::_thesis: ( X is bounded_below implies inf X in REAL )
given r being real number  such that A1: r is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: inf X in REAL
consider s being real number  such that
A2: s in X by MEMBERED:9;
A3: inf X <= s by A2, Th3;
A4: r in REAL by XREAL_0:def_1;
A5: s in REAL by XREAL_0:def_1;
 r <= inf X by A1, Def4;
hence  inf X in REAL by A4, A5, A3, XXREAL_0:45; ::_thesis: verum
end;

theorem Th16: :: XXREAL_2:16
for X being real-membered non empty set st X is bounded_above holds
sup X in REAL
proof
let X be real-membered non empty set ; ::_thesis: ( X is bounded_above implies sup X in REAL )
given r being real number  such that A1: r is UpperBound of X ; :: according to XXREAL_2:def_10 ::_thesis: sup X in REAL
consider s being real number  such that
A2: s in X by MEMBERED:9;
A3: s <= sup X by A2, Th4;
A4: r in REAL by XREAL_0:def_1;
A5: s in REAL by XREAL_0:def_1;
 sup X <= r by A1, Def3;
hence  sup X in REAL by A4, A5, A3, XXREAL_0:45; ::_thesis: verum
end;

registration
let X be real-membered non empty bounded_above set ;
cluster sup X ->  ext-real real ;
coherence
 sup X is real
proof
 sup X in REAL by Th16;
hence  sup X is real ; ::_thesis: verum
end;
end;

registration
let X be real-membered non empty bounded_below set ;
cluster inf X ->  ext-real real ;
coherence
 inf X is real
proof
 inf X in REAL by Th15;
hence  inf X is real ; ::_thesis: verum
end;
end;

registration
cluster integer-membered non empty bounded_above  ->  integer-membered non empty right_end for set ;
coherence
 for b1 being integer-membered non empty set st b1 is bounded_above holds
b1 is right_end
proof
let X be integer-membered non empty set ; ::_thesis: ( X is bounded_above implies X is right_end )
assume  X is bounded_above ; ::_thesis: X is right_end
then reconsider Y = X as integer-membered non empty bounded_above set ;
set s = sup Y;
A1: [\(sup Y)/] <= sup Y by INT_1:def_6;
 [\(sup Y)/] is UpperBound of X
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= [\(sup Y)/] )
assume  x in X ; ::_thesis: x <= [\(sup Y)/]
hence  x <= [\(sup Y)/] by Th4, INT_1:54; ::_thesis: verum
end;
then  sup Y <= [\(sup Y)/] by Def3;
then reconsider s = sup Y as Integer by A1, XXREAL_0:1;
assume A2: not sup X in X ; :: according to XXREAL_2:def_6 ::_thesis: contradiction
 s - 1 is UpperBound of X
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= s - 1 )
assume A3: x in X ; ::_thesis: x <= s - 1
then reconsider i = x as Integer ;
 i <= s by A3, Th4;
then  i < s by A2, A3, XXREAL_0:1;
hence  x <= s - 1 by INT_1:52; ::_thesis: verum
end;
then  s - 1 >= s by Def3;
hence  contradiction by XREAL_1:146; ::_thesis: verum
end;
end;

registration
cluster integer-membered non empty bounded_below  ->  integer-membered non empty left_end for set ;
coherence
 for b1 being integer-membered non empty set st b1 is bounded_below holds
b1 is left_end
proof
let X be integer-membered non empty set ; ::_thesis: ( X is bounded_below implies X is left_end )
assume  X is bounded_below ; ::_thesis: X is left_end
then reconsider Y = X as integer-membered non empty bounded_below set ;
set s = inf Y;
A1: [/(inf Y)\] >= inf Y by INT_1:def_7;
 [/(inf Y)\] is LowerBound of X
proof
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies [/(inf Y)\] <= x )
assume  x in X ; ::_thesis: [/(inf Y)\] <= x
hence  [/(inf Y)\] <= x by Th3, INT_1:65; ::_thesis: verum
end;
then  [/(inf Y)\] <= inf Y by Def4;
then reconsider s = inf Y as Integer by A1, XXREAL_0:1;
assume A2: not inf X in X ; :: according to XXREAL_2:def_5 ::_thesis: contradiction
 s + 1 is LowerBound of X
proof
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies s + 1 <= x )
assume A3: x in X ; ::_thesis: s + 1 <= x
then reconsider i = x as Integer ;
 i >= s by A3, Th3;
then  s < i by A2, A3, XXREAL_0:1;
hence  s + 1 <= x by INT_1:7; ::_thesis: verum
end;
then  s + 1 <= s by Def4;
hence  contradiction by XREAL_1:145; ::_thesis: verum
end;
end;

registration
cluster natural-membered  ->  natural-membered bounded_below for set ;
coherence
 for b1 being natural-membered set holds b1 is bounded_below
proof
let X be natural-membered set ; ::_thesis: X is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies 0 <= x )
assume  x in X ; ::_thesis: 0 <= x
hence  0 <= x ; ::_thesis: verum
end;
end;

registration
let X be real-membered left_end set ;
cluster inf X ->  ext-real real ;
coherence
 min X is real
proof
 min X in X by Def7;
hence  min X is real ; ::_thesis: verum
end;
end;

registration
let X be rational-membered left_end set ;
cluster inf X ->  ext-real rational ;
coherence
 min X is rational
proof
 min X in X by Def7;
hence  min X is rational ; ::_thesis: verum
end;
end;

registration
let X be integer-membered left_end set ;
cluster inf X ->  ext-real integer ;
coherence
 min X is integer
proof
 min X in X by Def7;
hence  min X is integer ; ::_thesis: verum
end;
end;

registration
let X be natural-membered left_end set ;
cluster inf X ->  ext-real natural ;
coherence
 min X is natural
proof
 min X in X by Def7;
hence  min X is natural ; ::_thesis: verum
end;
end;

registration
let X be real-membered right_end set ;
cluster sup X ->  ext-real real ;
coherence
 max X is real
proof
 max X in X by Def8;
hence  max X is real ; ::_thesis: verum
end;
end;

registration
let X be rational-membered right_end set ;
cluster sup X ->  ext-real rational ;
coherence
 max X is rational
proof
 max X in X by Def8;
hence  max X is rational ; ::_thesis: verum
end;
end;

registration
let X be integer-membered right_end set ;
cluster sup X ->  ext-real integer ;
coherence
 max X is integer
proof
 max X in X by Def8;
hence  max X is integer ; ::_thesis: verum
end;
end;

registration
let X be natural-membered right_end set ;
cluster sup X ->  ext-real natural ;
coherence
 max X is natural
proof
 max X in X by Def8;
hence  max X is natural ; ::_thesis: verum
end;
end;

registration
cluster real-membered left_end  ->  real-membered bounded_below for set ;
coherence
 for b1 being real-membered set st b1 is left_end holds
b1 is bounded_below
proof
let X be real-membered set ; ::_thesis: ( X is left_end implies X is bounded_below )
assume  inf X in X ; :: according to XXREAL_2:def_5 ::_thesis: X is bounded_below
then reconsider r = inf X as real number ;
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies r <= x )
thus  ( x in X implies r <= x ) by Th3; ::_thesis: verum
end;
cluster real-membered right_end  ->  real-membered bounded_above for set ;
coherence
 for b1 being real-membered set st b1 is right_end holds
b1 is bounded_above
proof
let X be real-membered set ; ::_thesis: ( X is right_end implies X is bounded_above )
assume  sup X in X ; :: according to XXREAL_2:def_6 ::_thesis: X is bounded_above
then reconsider r = sup X as real number ;
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= r )
thus  ( x in X implies x <= r ) by Th4; ::_thesis: verum
end;
end;

theorem Th17: :: XXREAL_2:17
for x, y being ext-real number holds x is LowerBound of [.x,y.]
proof
let x, y be ext-real number ; ::_thesis: x is LowerBound of [.x,y.]
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in [.x,y.] implies x <= z )
assume  z in [.x,y.] ; ::_thesis: x <= z
hence  x <= z by XXREAL_1:1; ::_thesis: verum
end;

theorem Th18: :: XXREAL_2:18
for x, y being ext-real number holds x is LowerBound of ].x,y.]
proof
let x, y be ext-real number ; ::_thesis: x is LowerBound of ].x,y.]
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in ].x,y.] implies x <= z )
assume  z in ].x,y.] ; ::_thesis: x <= z
hence  x <= z by XXREAL_1:2; ::_thesis: verum
end;

theorem Th19: :: XXREAL_2:19
for x, y being ext-real number holds x is LowerBound of [.x,y.[
proof
let x, y be ext-real number ; ::_thesis: x is LowerBound of [.x,y.[
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in [.x,y.[ implies x <= z )
assume  z in [.x,y.[ ; ::_thesis: x <= z
hence  x <= z by XXREAL_1:3; ::_thesis: verum
end;

theorem Th20: :: XXREAL_2:20
for x, y being ext-real number holds x is LowerBound of ].x,y.[
proof
let x, y be ext-real number ; ::_thesis: x is LowerBound of ].x,y.[
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in ].x,y.[ implies x <= z )
assume  z in ].x,y.[ ; ::_thesis: x <= z
hence  x <= z by XXREAL_1:4; ::_thesis: verum
end;

theorem Th21: :: XXREAL_2:21
for y, x being ext-real number holds y is UpperBound of [.x,y.]
proof
let y, x be ext-real number ; ::_thesis: y is UpperBound of [.x,y.]
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in [.x,y.] implies z <= y )
assume  z in [.x,y.] ; ::_thesis: z <= y
hence  z <= y by XXREAL_1:1; ::_thesis: verum
end;

theorem Th22: :: XXREAL_2:22
for y, x being ext-real number holds y is UpperBound of ].x,y.]
proof
let y, x be ext-real number ; ::_thesis: y is UpperBound of ].x,y.]
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in ].x,y.] implies z <= y )
assume  z in ].x,y.] ; ::_thesis: z <= y
hence  z <= y by XXREAL_1:2; ::_thesis: verum
end;

theorem Th23: :: XXREAL_2:23
for y, x being ext-real number holds y is UpperBound of [.x,y.[
proof
let y, x be ext-real number ; ::_thesis: y is UpperBound of [.x,y.[
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in [.x,y.[ implies z <= y )
assume  z in [.x,y.[ ; ::_thesis: z <= y
hence  z <= y by XXREAL_1:3; ::_thesis: verum
end;

theorem Th24: :: XXREAL_2:24
for y, x being ext-real number holds y is UpperBound of ].x,y.[
proof
let y, x be ext-real number ; ::_thesis: y is UpperBound of ].x,y.[
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in ].x,y.[ implies z <= y )
assume  z in ].x,y.[ ; ::_thesis: z <= y
hence  z <= y by XXREAL_1:4; ::_thesis: verum
end;

theorem Th25: :: XXREAL_2:25
for x, y being ext-real number st x <= y holds
inf [.x,y.] = x
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies inf [.x,y.] = x )
assume A1: x <= y ; ::_thesis: inf [.x,y.] = x
A2: for z being LowerBound of [.x,y.] holds z <= x
proof
let z be LowerBound of [.x,y.]; ::_thesis: z <= x
 x in [.x,y.] by A1, XXREAL_1:1;
hence  z <= x by Def2; ::_thesis: verum
end;
 x is LowerBound of [.x,y.] by Th17;
hence  inf [.x,y.] = x by A2, Def4; ::_thesis: verum
end;

theorem Th26: :: XXREAL_2:26
for x, y being ext-real number st x < y holds
inf [.x,y.[ = x
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies inf [.x,y.[ = x )
assume A1: x < y ; ::_thesis: inf [.x,y.[ = x
A2: for z being LowerBound of [.x,y.[ holds z <= x
proof
let z be LowerBound of [.x,y.[; ::_thesis: z <= x
 x in [.x,y.[ by A1, XXREAL_1:3;
hence  z <= x by Def2; ::_thesis: verum
end;
 x is LowerBound of [.x,y.[ by Th19;
hence  inf [.x,y.[ = x by A2, Def4; ::_thesis: verum
end;

theorem Th27: :: XXREAL_2:27
for x, y being ext-real number st x < y holds
inf ].x,y.] = x
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies inf ].x,y.] = x )
assume A1: x < y ; ::_thesis: inf ].x,y.] = x
A2: for z being LowerBound of ].x,y.] holds z <= x
proof
let z be LowerBound of ].x,y.]; ::_thesis: z <= x
 for r being ext-real number st x < r & r < y holds
z <= r
proof
let r be ext-real number ; ::_thesis: ( x < r & r < y implies z <= r )
assume that
A3: x < r and
A4: r < y ; ::_thesis: z <= r
 r in ].x,y.] by A3, A4, XXREAL_1:2;
hence  z <= r by Def2; ::_thesis: verum
end;
hence  z <= x by A1, XREAL_1:228; ::_thesis: verum
end;
 x is LowerBound of ].x,y.] by Th18;
hence  inf ].x,y.] = x by A2, Def4; ::_thesis: verum
end;

theorem Th28: :: XXREAL_2:28
for x, y being ext-real number st x < y holds
inf ].x,y.[ = x
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies inf ].x,y.[ = x )
assume A1: x < y ; ::_thesis: inf ].x,y.[ = x
A2: for z being LowerBound of ].x,y.[ holds z <= x
proof
let z be LowerBound of ].x,y.[; ::_thesis: z <= x
 for r being ext-real number st x < r & r < y holds
z <= r
proof
let r be ext-real number ; ::_thesis: ( x < r & r < y implies z <= r )
assume that
A3: x < r and
A4: r < y ; ::_thesis: z <= r
 r in ].x,y.[ by A3, A4, XXREAL_1:4;
hence  z <= r by Def2; ::_thesis: verum
end;
hence  z <= x by A1, XREAL_1:228; ::_thesis: verum
end;
 x is LowerBound of ].x,y.[ by Th20;
hence  inf ].x,y.[ = x by A2, Def4; ::_thesis: verum
end;

theorem Th29: :: XXREAL_2:29
for x, y being ext-real number st x <= y holds
sup [.x,y.] = y
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies sup [.x,y.] = y )
assume A1: x <= y ; ::_thesis: sup [.x,y.] = y
A2: for z being UpperBound of [.x,y.] holds y <= z
proof
let z be UpperBound of [.x,y.]; ::_thesis: y <= z
 y in [.x,y.] by A1, XXREAL_1:1;
hence  y <= z by Def1; ::_thesis: verum
end;
 y is UpperBound of [.x,y.] by Th21;
hence  sup [.x,y.] = y by A2, Def3; ::_thesis: verum
end;

theorem Th30: :: XXREAL_2:30
for x, y being ext-real number st x < y holds
sup ].x,y.] = y
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies sup ].x,y.] = y )
assume A1: x < y ; ::_thesis: sup ].x,y.] = y
A2: for z being UpperBound of ].x,y.] holds y <= z
proof
let z be UpperBound of ].x,y.]; ::_thesis: y <= z
 y in ].x,y.] by A1, XXREAL_1:2;
hence  y <= z by Def1; ::_thesis: verum
end;
 y is UpperBound of ].x,y.] by Th22;
hence  sup ].x,y.] = y by A2, Def3; ::_thesis: verum
end;

theorem Th31: :: XXREAL_2:31
for x, y being ext-real number st x < y holds
sup [.x,y.[ = y
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies sup [.x,y.[ = y )
assume A1: x < y ; ::_thesis: sup [.x,y.[ = y
A2: for z being UpperBound of [.x,y.[ holds y <= z
proof
let z be UpperBound of [.x,y.[; ::_thesis: y <= z
 for r being ext-real number st x < r & r < y holds
r <= z
proof
let r be ext-real number ; ::_thesis: ( x < r & r < y implies r <= z )
assume that
A3: x < r and
A4: r < y ; ::_thesis: r <= z
 r in [.x,y.[ by A3, A4, XXREAL_1:3;
hence  r <= z by Def1; ::_thesis: verum
end;
hence  y <= z by A1, XREAL_1:229; ::_thesis: verum
end;
 y is UpperBound of [.x,y.[ by Th23;
hence  sup [.x,y.[ = y by A2, Def3; ::_thesis: verum
end;

theorem Th32: :: XXREAL_2:32
for x, y being ext-real number st x < y holds
sup ].x,y.[ = y
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies sup ].x,y.[ = y )
assume A1: x < y ; ::_thesis: sup ].x,y.[ = y
A2: for z being UpperBound of ].x,y.[ holds y <= z
proof
let z be UpperBound of ].x,y.[; ::_thesis: y <= z
 for r being ext-real number st x < r & r < y holds
r <= z
proof
let r be ext-real number ; ::_thesis: ( x < r & r < y implies r <= z )
assume that
A3: x < r and
A4: r < y ; ::_thesis: r <= z
 r in ].x,y.[ by A3, A4, XXREAL_1:4;
hence  r <= z by Def1; ::_thesis: verum
end;
hence  y <= z by A1, XREAL_1:229; ::_thesis: verum
end;
 y is UpperBound of ].x,y.[ by Th24;
hence  sup ].x,y.[ = y by A2, Def3; ::_thesis: verum
end;

theorem Th33: :: XXREAL_2:33
for x, y being ext-real number st x <= y holds
( [.x,y.] is left_end & [.x,y.] is right_end )
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies ( [.x,y.] is left_end & [.x,y.] is right_end ) )
assume A1: x <= y ; ::_thesis: ( [.x,y.] is left_end & [.x,y.] is right_end )
then  x in [.x,y.] by XXREAL_1:1;
then  inf [.x,y.] in [.x,y.] by A1, Th25;
hence  [.x,y.] is left_end by Def5; ::_thesis: [.x,y.] is right_end
 y in [.x,y.] by A1, XXREAL_1:1;
hence  sup [.x,y.] in [.x,y.] by A1, Th29; :: according to XXREAL_2:def_6 ::_thesis: verum
end;

theorem Th34: :: XXREAL_2:34
for x, y being ext-real number st x < y holds
[.x,y.[ is left_end
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies [.x,y.[ is left_end )
assume A1: x < y ; ::_thesis: [.x,y.[ is left_end
then  x in [.x,y.[ by XXREAL_1:3;
hence  inf [.x,y.[ in [.x,y.[ by A1, Th26; :: according to XXREAL_2:def_5 ::_thesis: verum
end;

theorem Th35: :: XXREAL_2:35
for x, y being ext-real number st x < y holds
].x,y.] is right_end
proof
let x, y be ext-real number ; ::_thesis: ( x < y implies ].x,y.] is right_end )
assume A1: x < y ; ::_thesis: ].x,y.] is right_end
then  y in ].x,y.] by XXREAL_1:2;
hence  sup ].x,y.] in ].x,y.] by A1, Th30; :: according to XXREAL_2:def_6 ::_thesis: verum
end;

theorem Th36: :: XXREAL_2:36
for x being ext-real number holds x is LowerBound of {}
proof
let x be ext-real number ; ::_thesis: x is LowerBound of {}
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( y in {} implies x <= y )
thus  ( y in {} implies x <= y ) ; ::_thesis: verum
end;

theorem Th37: :: XXREAL_2:37
for x being ext-real number holds x is UpperBound of {}
proof
let x be ext-real number ; ::_thesis: x is UpperBound of {}
let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( y in {} implies y <= x )
thus  ( y in {} implies y <= x ) ; ::_thesis: verum
end;

theorem Th38: :: XXREAL_2:38
inf {} = +infty
proof
A1: for x being LowerBound of {} holds x <= +infty by XXREAL_0:3;
 +infty is LowerBound of {} by Th36;
hence  inf {} = +infty by A1, Def4; ::_thesis: verum
end;

theorem Th39: :: XXREAL_2:39
sup {} = -infty
proof
A1: for x being UpperBound of {} holds -infty <= x by XXREAL_0:5;
 -infty is UpperBound of {} by Th37;
hence  sup {} = -infty by A1, Def3; ::_thesis: verum
end;

theorem Th40: :: XXREAL_2:40
for X being ext-real-membered set holds
( not X is empty iff inf X <= sup X )
proof
let X be ext-real-membered set ; ::_thesis: ( not X is empty iff inf X <= sup X )
thus  ( not X is empty implies inf X <= sup X ) ::_thesis: ( inf X <= sup X implies not X is empty )
proof
assume  not X is empty ; ::_thesis: inf X <= sup X
then consider x being ext-real number  such that
A1: x in X by MEMBERED:8;
A2: x <= sup X by A1, Th4;
 inf X <= x by A1, Th3;
hence  inf X <= sup X by A2, XXREAL_0:2; ::_thesis: verum
end;
assume  inf X <= sup X ; ::_thesis: not X is empty
hence  not X is empty by Th38, Th39; ::_thesis: verum
end;

registration
cluster integer-membered real-bounded  ->  integer-membered finite for set ;
coherence
 for b1 being integer-membered set st b1 is real-bounded holds
b1 is finite
proof
let X be integer-membered set ; ::_thesis: ( X is real-bounded implies X is finite )
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: ( X is real-bounded implies X is finite )
hence  ( X is real-bounded implies X is finite ) ; ::_thesis: verum
end;
supposeA1: not X is empty ; ::_thesis: ( X is real-bounded implies X is finite )
assume  ( X is bounded_below & X is bounded_above ) ; :: according to XXREAL_2:def_11 ::_thesis: X is finite
then reconsider Z = X as integer-membered non empty bounded_below bounded_above set by A1;
set m = inf Z;
set n = sup Z;
defpred S1[ set ] means c1 in X;
deffunc H1( set ) ->  set = c1;
set Y =  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }  ;
A2: X c=  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }
proof
let i be Integer; :: according to MEMBERED:def_11 ::_thesis: ( not i in X or i in  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }  )
A3: i in INT by INT_1:def_2;
assume A4: S1[i] ; ::_thesis: i in  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }
then A5: i <= sup Z by Th4;
 inf Z <= i by A4, Th3;
hence  i in  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }  by A3, A4, A5; ::_thesis: verum
end;
  {  H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] )  }  is finite from XXREAL_2:sch_1();
hence  X is finite by A2; ::_thesis: verum
end;
end;
end;
end;

registration
cluster natural-membered bounded_above  ->  natural-membered finite bounded_above for set ;
coherence
 for b1 being natural-membered bounded_above set holds b1 is finite ;
end;

theorem :: XXREAL_2:41
for X being ext-real-membered set holds +infty is UpperBound of X
proof
let X be ext-real-membered set ; ::_thesis: +infty is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= +infty )
assume  x in X ; ::_thesis: x <= +infty
thus  x <= +infty by XXREAL_0:3; ::_thesis: verum
end;

theorem :: XXREAL_2:42
for X being ext-real-membered set holds -infty is LowerBound of X
proof
let X be ext-real-membered set ; ::_thesis: -infty is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies -infty <= x )
assume  x in X ; ::_thesis: -infty <= x
thus  -infty <= x by XXREAL_0:5; ::_thesis: verum
end;

theorem Th43: :: XXREAL_2:43
for X, Y being ext-real-membered set st X c= Y & Y is bounded_above holds
X is bounded_above
proof
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y & Y is bounded_above implies X is bounded_above )
assume A1: X c= Y ; ::_thesis: ( not Y is bounded_above or X is bounded_above )
given r being real number  such that A2: r is UpperBound of Y ; :: according to XXREAL_2:def_10 ::_thesis: X is bounded_above
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
thus  r is UpperBound of X by A1, A2, Th6; ::_thesis: verum
end;

theorem Th44: :: XXREAL_2:44
for X, Y being ext-real-membered set st X c= Y & Y is bounded_below holds
X is bounded_below
proof
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y & Y is bounded_below implies X is bounded_below )
assume A1: X c= Y ; ::_thesis: ( not Y is bounded_below or X is bounded_below )
given r being real number  such that A2: r is LowerBound of Y ; :: according to XXREAL_2:def_9 ::_thesis: X is bounded_below
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of X
thus  r is LowerBound of X by A1, A2, Th5; ::_thesis: verum
end;

theorem :: XXREAL_2:45
for X, Y being ext-real-membered set st X c= Y & Y is real-bounded holds
X is real-bounded
proof
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y & Y is real-bounded implies X is real-bounded )
assume A1: X c= Y ; ::_thesis: ( not Y is real-bounded or X is real-bounded )
assume  ( Y is bounded_below & Y is bounded_above ) ; :: according to XXREAL_2:def_11 ::_thesis: X is real-bounded
hence  ( X is bounded_below & X is bounded_above ) by A1, Th43, Th44; :: according to XXREAL_2:def_11 ::_thesis: verum
end;

theorem Th46: :: XXREAL_2:46
( not REAL is bounded_below & not REAL is bounded_above )
proof
thus  not REAL is bounded_below ::_thesis: not REAL is bounded_above
proof
given r being real number  such that A1: r is LowerBound of REAL ; :: according to XXREAL_2:def_9 ::_thesis: contradiction
consider s being real number  such that
A2: s < r by XREAL_1:2;
 s in REAL by XREAL_0:def_1;
hence  contradiction by A1, A2, Def2; ::_thesis: verum
end;
given r being real number  such that A3: r is UpperBound of REAL ; :: according to XXREAL_2:def_10 ::_thesis: contradiction
consider s being real number  such that
A4: r < s by XREAL_1:1;
 s in REAL by XREAL_0:def_1;
hence  contradiction by A3, A4, Def1; ::_thesis: verum
end;

registration
cluster REAL  ->  non bounded_below non bounded_above ;
coherence
 ( not REAL is bounded_below & not REAL is bounded_above ) by Th46;
end;

theorem :: XXREAL_2:47
{+infty} is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of {+infty}
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in {+infty} implies 0 <= x )
assume  x in {+infty} ; ::_thesis: 0 <= x
hence  0 <= x by TARSKI:def_1; ::_thesis: verum
end;

theorem :: XXREAL_2:48
{-infty} is bounded_above
proof
take  0 ; :: according to XXREAL_2:def_10 ::_thesis: 0 is UpperBound of {-infty}
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in {-infty} implies x <= 0 )
assume  x in {-infty} ; ::_thesis: x <= 0
hence  x <= 0 by TARSKI:def_1; ::_thesis: verum
end;

theorem Th49: :: XXREAL_2:49
for X being ext-real-membered non empty bounded_above set st X <> {-infty} holds
ex x being Element of REAL st x in X
proof
let X be ext-real-membered non empty bounded_above set ; ::_thesis: ( X <> {-infty} implies ex x being Element of REAL st x in X )
assume  X <> {-infty} ; ::_thesis: ex x being Element of REAL st x in X
then consider x being set  such that
A1: x in X and
A2: x <> -infty by ZFMISC_1:35;
reconsider x = x as ext-real number by A1;
consider r being real number  such that
A3: r is UpperBound of X by Def10;
A4: r in REAL by XREAL_0:def_1;
 x <= r by A3, A1, Def1;
then  x in REAL by A4, A2, XXREAL_0:13;
hence  ex x being Element of REAL st x in X by A1; ::_thesis: verum
end;

theorem Th50: :: XXREAL_2:50
for X being ext-real-membered non empty bounded_below set st X <> {+infty} holds
ex x being Element of REAL st x in X
proof
let X be ext-real-membered non empty bounded_below set ; ::_thesis: ( X <> {+infty} implies ex x being Element of REAL st x in X )
assume  X <> {+infty} ; ::_thesis: ex x being Element of REAL st x in X
then consider x being set  such that
A1: x in X and
A2: x <> +infty by ZFMISC_1:35;
reconsider x = x as ext-real number by A1;
consider r being real number  such that
A3: r is LowerBound of X by Def9;
A4: r in REAL by XREAL_0:def_1;
 r <= x by A3, A1, Def2;
then  x in REAL by A4, A2, XXREAL_0:10;
hence  ex x being Element of REAL st x in X by A1; ::_thesis: verum
end;

theorem Th51: :: XXREAL_2:51
for X being ext-real-membered set st -infty is UpperBound of X holds
X c= {-infty}
proof
let X be ext-real-membered set ; ::_thesis: ( -infty is UpperBound of X implies X c= {-infty} )
assume A1: -infty is UpperBound of X ; ::_thesis: X c= {-infty}
let x be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not x in X or x in {-infty} )
assume  x in X ; ::_thesis: x in {-infty}
then  x = -infty by A1, Def1, XXREAL_0:6;
hence  x in {-infty} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th52: :: XXREAL_2:52
for X being ext-real-membered set st +infty is LowerBound of X holds
X c= {+infty}
proof
let X be ext-real-membered set ; ::_thesis: ( +infty is LowerBound of X implies X c= {+infty} )
assume A1: +infty is LowerBound of X ; ::_thesis: X c= {+infty}
let x be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not x in X or x in {+infty} )
assume  x in X ; ::_thesis: x in {+infty}
then  x = +infty by A1, Def2, XXREAL_0:4;
hence  x in {+infty} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: XXREAL_2:53
for X being ext-real-membered non empty set st ex y being UpperBound of X st y <> +infty holds
X is bounded_above
proof
let X be ext-real-membered non empty set ; ::_thesis: ( ex y being UpperBound of X st y <> +infty implies X is bounded_above )
given y being UpperBound of X such that A1: y <> +infty ; ::_thesis: X is bounded_above
percases ( y = -infty or y <> -infty ) ;
supposeA2: y = -infty ; ::_thesis: X is bounded_above
take  0 ; :: according to XXREAL_2:def_10 ::_thesis: 0 is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= 0 )
assume A3: x in X ; ::_thesis: x <= 0
 X c= {-infty} by A2, Th51;
hence  x <= 0 by A3, TARSKI:def_1; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: X is bounded_above
then  y in REAL by A1, XXREAL_0:14;
then reconsider y = y as real number ;
take  y ; :: according to XXREAL_2:def_10 ::_thesis: y is UpperBound of X
thus  y is UpperBound of X ; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:54
for X being ext-real-membered non empty set st ex y being LowerBound of X st y <> -infty holds
X is bounded_below
proof
let X be ext-real-membered non empty set ; ::_thesis: ( ex y being LowerBound of X st y <> -infty implies X is bounded_below )
given y being LowerBound of X such that A1: y <> -infty ; ::_thesis: X is bounded_below
percases ( y = +infty or y <> +infty ) ;
supposeA2: y = +infty ; ::_thesis: X is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in X implies 0 <= x )
assume A3: x in X ; ::_thesis: 0 <= x
 X c= {+infty} by A2, Th52;
hence  0 <= x by A3, TARSKI:def_1; ::_thesis: verum
end;
suppose y <> +infty ; ::_thesis: X is bounded_below
then  y in REAL by A1, XXREAL_0:14;
then reconsider y = y as real number ;
take  y ; :: according to XXREAL_2:def_9 ::_thesis: y is LowerBound of X
thus  y is LowerBound of X ; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:55
for X being ext-real-membered non empty set
for x being UpperBound of X st x in X holds
x = sup X
proof
let X be ext-real-membered non empty set ; ::_thesis: for x being UpperBound of X st x in X holds
x = sup X
let x be UpperBound of X; ::_thesis: ( x in X implies x = sup X )
assume  x in X ; ::_thesis: x = sup X
then  for y being UpperBound of X holds x <= y by Def1;
hence  x = sup X by Def3; ::_thesis: verum
end;

theorem :: XXREAL_2:56
for X being ext-real-membered non empty set
for x being LowerBound of X st x in X holds
x = inf X
proof
let X be ext-real-membered non empty set ; ::_thesis: for x being LowerBound of X st x in X holds
x = inf X
let x be LowerBound of X; ::_thesis: ( x in X implies x = inf X )
assume  x in X ; ::_thesis: x = inf X
then  for y being LowerBound of X holds y <= x by Def2;
hence  x = inf X by Def4; ::_thesis: verum
end;

theorem Th57: :: XXREAL_2:57
for X being ext-real-membered non empty set st X is bounded_above & X <> {-infty} holds
sup X in REAL
proof
let X be ext-real-membered non empty set ; ::_thesis: ( X is bounded_above & X <> {-infty} implies sup X in REAL )
assume A1: X is bounded_above ; ::_thesis: ( not X <> {-infty} or sup X in REAL )
then consider r being real number  such that
A2: r is UpperBound of X by Def10;
assume  X <> {-infty} ; ::_thesis: sup X in REAL
then A3: ex x being Element of REAL st x in X by A1, Th49;
 sup X is UpperBound of X by Def3;
then A4: not sup X = -infty by A3, Def1, XXREAL_0:12;
A5: r in REAL by XREAL_0:def_1;
 sup X <= r by A2, Def3;
hence  sup X in REAL by A5, A4, XXREAL_0:13; ::_thesis: verum
end;

theorem Th58: :: XXREAL_2:58
for X being ext-real-membered non empty set st X is bounded_below & X <> {+infty} holds
inf X in REAL
proof
let X be ext-real-membered non empty set ; ::_thesis: ( X is bounded_below & X <> {+infty} implies inf X in REAL )
assume A1: X is bounded_below ; ::_thesis: ( not X <> {+infty} or inf X in REAL )
then consider r being real number  such that
A2: r is LowerBound of X by Def9;
assume  X <> {+infty} ; ::_thesis: inf X in REAL
then A3: ex x being Element of REAL st x in X by A1, Th50;
 inf X is LowerBound of X by Def4;
then A4: inf X <> +infty by A3, Def2, XXREAL_0:9;
A5: r in REAL by XREAL_0:def_1;
 r <= inf X by A2, Def4;
hence  inf X in REAL by A5, A4, XXREAL_0:10; ::_thesis: verum
end;

theorem :: XXREAL_2:59
for X, Y being ext-real-membered set st X c= Y holds
sup X <= sup Y
proof
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies sup X <= sup Y )
assume A1: X c= Y ; ::_thesis: sup X <= sup Y
 sup Y is UpperBound of Y by Def3;
then  sup Y is UpperBound of X by A1, Th6;
hence  sup X <= sup Y by Def3; ::_thesis: verum
end;

theorem :: XXREAL_2:60
for X, Y being ext-real-membered set st X c= Y holds
inf Y <= inf X
proof
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies inf Y <= inf X )
assume A1: X c= Y ; ::_thesis: inf Y <= inf X
 inf Y is LowerBound of Y by Def4;
then  inf Y is LowerBound of X by A1, Th5;
hence  inf Y <= inf X by Def4; ::_thesis: verum
end;

theorem :: XXREAL_2:61
for X being ext-real-membered set
for x being ext-real number st ex y being ext-real number st
( y in X & x <= y ) holds
x <= sup X
proof
let X be ext-real-membered set ; ::_thesis: for x being ext-real number st ex y being ext-real number st
( y in X & x <= y ) holds
x <= sup X
let x be ext-real number ; ::_thesis: ( ex y being ext-real number st
( y in X & x <= y ) implies x <= sup X )
given y being ext-real number  such that A1: y in X and
A2: x <= y ; ::_thesis: x <= sup X
 y <= sup X by A1, Th4;
hence  x <= sup X by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XXREAL_2:62
for X being ext-real-membered set
for x being ext-real number st ex y being ext-real number st
( y in X & y <= x ) holds
inf X <= x
proof
let X be ext-real-membered set ; ::_thesis: for x being ext-real number st ex y being ext-real number st
( y in X & y <= x ) holds
inf X <= x
let x be ext-real number ; ::_thesis: ( ex y being ext-real number st
( y in X & y <= x ) implies inf X <= x )
given y being ext-real number  such that A1: y in X and
A2: y <= x ; ::_thesis: inf X <= x
 inf X <= y by A1, Th3;
hence  inf X <= x by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XXREAL_2:63
for X, Y being ext-real-membered set st ( for x being ext-real number st x in X holds
ex y being ext-real number st
( y in Y & x <= y ) ) holds
sup X <= sup Y
proof
let X, Y be ext-real-membered set ; ::_thesis: ( ( for x being ext-real number st x in X holds
ex y being ext-real number st
( y in Y & x <= y ) ) implies sup X <= sup Y )
assume A1: for x being ext-real number st x in X holds
ex y being ext-real number st
( y in Y & x <= y ) ; ::_thesis: sup X <= sup Y
 sup Y is UpperBound of X
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in X implies x <= sup Y )
assume  x in X ; ::_thesis: x <= sup Y
then consider y being ext-real number  such that
A2: y in Y and
A3: x <= y by A1;
 y <= sup Y by A2, Th4;
hence  x <= sup Y by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  sup X <= sup Y by Def3; ::_thesis: verum
end;

theorem :: XXREAL_2:64
for X, Y being ext-real-membered set st ( for y being ext-real number st y in Y holds
ex x being ext-real number st
( x in X & x <= y ) ) holds
inf X <= inf Y
proof
let X, Y be ext-real-membered set ; ::_thesis: ( ( for y being ext-real number st y in Y holds
ex x being ext-real number st
( x in X & x <= y ) ) implies inf X <= inf Y )
assume A1: for y being ext-real number st y in Y holds
ex x being ext-real number st
( x in X & x <= y ) ; ::_thesis: inf X <= inf Y
 inf X is LowerBound of Y
proof
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( y in Y implies inf X <= y )
assume  y in Y ; ::_thesis: inf X <= y
then consider x being ext-real number  such that
A2: x in X and
A3: x <= y by A1;
 inf X <= x by A2, Th3;
hence  inf X <= y by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  inf X <= inf Y by Def4; ::_thesis: verum
end;

theorem Th65: :: XXREAL_2:65
for X, Y being ext-real-membered set
for x being UpperBound of X
for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y
proof
let X, Y be ext-real-membered set ; ::_thesis: for x being UpperBound of X
for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y
let x be UpperBound of X; ::_thesis: for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y
let y be UpperBound of Y; ::_thesis: min (x,y) is UpperBound of X /\ Y
let a be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( a in X /\ Y implies a <= min (x,y) )
assume A1: a in X /\ Y ; ::_thesis: a <= min (x,y)
then  a in Y by XBOOLE_0:def_4;
then A2: a <= y by Def1;
 a in X by A1, XBOOLE_0:def_4;
then  a <= x by Def1;
hence  a <= min (x,y) by A2, XXREAL_0:20; ::_thesis: verum
end;

theorem Th66: :: XXREAL_2:66
for X, Y being ext-real-membered set
for x being LowerBound of X
for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y
proof
let X, Y be ext-real-membered set ; ::_thesis: for x being LowerBound of X
for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y
let x be LowerBound of X; ::_thesis: for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y
let y be LowerBound of Y; ::_thesis: max (x,y) is LowerBound of X /\ Y
let a be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( a in X /\ Y implies max (x,y) <= a )
assume A1: a in X /\ Y ; ::_thesis: max (x,y) <= a
then  a in Y by XBOOLE_0:def_4;
then A2: y <= a by Def2;
 a in X by A1, XBOOLE_0:def_4;
then  x <= a by Def2;
hence  max (x,y) <= a by A2, XXREAL_0:28; ::_thesis: verum
end;

theorem :: XXREAL_2:67
for X, Y being ext-real-membered set holds sup (X /\ Y) <= min ((sup X),(sup Y))
proof
let X, Y be ext-real-membered set ; ::_thesis: sup (X /\ Y) <= min ((sup X),(sup Y))
A1: sup Y is UpperBound of Y by Def3;
 sup X is UpperBound of X by Def3;
then  min ((sup X),(sup Y)) is UpperBound of X /\ Y by A1, Th65;
hence  sup (X /\ Y) <= min ((sup X),(sup Y)) by Def3; ::_thesis: verum
end;

theorem :: XXREAL_2:68
for X, Y being ext-real-membered set holds max ((inf X),(inf Y)) <= inf (X /\ Y)
proof
let X, Y be ext-real-membered set ; ::_thesis: max ((inf X),(inf Y)) <= inf (X /\ Y)
A1: inf Y is LowerBound of Y by Def4;
 inf X is LowerBound of X by Def4;
then  max ((inf X),(inf Y)) is LowerBound of X /\ Y by A1, Th66;
hence  max ((inf X),(inf Y)) <= inf (X /\ Y) by Def4; ::_thesis: verum
end;

registration
cluster ext-real-membered real-bounded  ->  ext-real-membered real-membered for set ;
coherence
 for b1 being ext-real-membered set st b1 is real-bounded holds
b1 is real-membered
proof
let X be ext-real-membered set ; ::_thesis: ( X is real-bounded implies X is real-membered )
assume A1: X is real-bounded ; ::_thesis: X is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( not x in X or x is real )
assume A2: x in X ; ::_thesis: x is real
then reconsider X = X as ext-real-membered non empty set ;
consider s being real number  such that
A3: s is UpperBound of X by A1, Def10;
reconsider x = x as ext-real number by A2;
A4: s in REAL by XREAL_0:def_1;
A5: x <= s by A2, A3, Def1;
consider r being real number  such that
A6: r is LowerBound of X by A1, Def9;
A7: r in REAL by XREAL_0:def_1;
 r <= x by A2, A6, Def2;
then  x in REAL by A5, A7, A4, XXREAL_0:45;
hence  x is real ; ::_thesis: verum
end;
end;

theorem Th69: :: XXREAL_2:69
for A being ext-real-membered set holds A c= [.(inf A),(sup A).]
proof
let A be ext-real-membered set ; ::_thesis: A c= [.(inf A),(sup A).]
let x be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not x in A or x in [.(inf A),(sup A).] )
assume A1: x in A ; ::_thesis: x in [.(inf A),(sup A).]
then A2: x <= sup A by Th4;
 inf A <= x by A1, Th3;
hence  x in [.(inf A),(sup A).] by A2, XXREAL_1:1; ::_thesis: verum
end;

theorem :: XXREAL_2:70
for A being ext-real-membered set st sup A = inf A holds
A = {(inf A)}
proof
let A be ext-real-membered set ; ::_thesis: ( sup A = inf A implies A = {(inf A)} )
assume A1: sup A = inf A ; ::_thesis: A = {(inf A)}
then  A c= [.(inf A),(inf A).] by Th69;
then A2: A c= {(inf A)} by XXREAL_1:17;
 A <> {} by A1, Th38, Th39;
hence  A = {(inf A)} by A2, ZFMISC_1:33; ::_thesis: verum
end;

theorem Th71: :: XXREAL_2:71
for x, y being ext-real number
for A being ext-real-membered set st x <= y & x is UpperBound of A holds
y is UpperBound of A
proof
let x, y be ext-real number ; ::_thesis: for A being ext-real-membered set st x <= y & x is UpperBound of A holds
y is UpperBound of A
let A be ext-real-membered set ; ::_thesis: ( x <= y & x is UpperBound of A implies y is UpperBound of A )
assume that
A1: x <= y and
A2: x is UpperBound of A ; ::_thesis: y is UpperBound of A
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( z in A implies z <= y )
assume  z in A ; ::_thesis: z <= y
then  z <= x by A2, Def1;
hence  z <= y by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th72: :: XXREAL_2:72
for y, x being ext-real number
for A being ext-real-membered set st y <= x & x is LowerBound of A holds
y is LowerBound of A
proof
let y, x be ext-real number ; ::_thesis: for A being ext-real-membered set st y <= x & x is LowerBound of A holds
y is LowerBound of A
let A be ext-real-membered set ; ::_thesis: ( y <= x & x is LowerBound of A implies y is LowerBound of A )
assume that
A1: y <= x and
A2: x is LowerBound of A ; ::_thesis: y is LowerBound of A
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( z in A implies y <= z )
assume  z in A ; ::_thesis: y <= z
then  x <= z by A2, Def2;
hence  y <= z by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XXREAL_2:73
for A being ext-real-membered set holds
( A is bounded_above iff sup A <> +infty )
proof
let A be ext-real-membered set ; ::_thesis: ( A is bounded_above iff sup A <> +infty )
hereby  ::_thesis: ( sup A <> +infty implies A is bounded_above )
assume A1: A is bounded_above ; ::_thesis: sup A <> +infty
percases ( A = {} or A = {-infty} or sup A in REAL ) by A1, Th57;
suppose A = {} ; ::_thesis: sup A <> +infty
hence  sup A <> +infty by Th39; ::_thesis: verum
end;
suppose A = {-infty} ; ::_thesis: sup A <> +infty
hence  sup A <> +infty by Lm1; ::_thesis: verum
end;
suppose sup A in REAL ; ::_thesis: sup A <> +infty
hence  sup A <> +infty ; ::_thesis: verum
end;
end;
end;
assume A2: sup A <> +infty ; ::_thesis: A is bounded_above
percases ( sup A = -infty or sup A in REAL ) by A2, XXREAL_0:14;
supposeA3: sup A = -infty ; ::_thesis: A is bounded_above
take  0 ; :: according to XXREAL_2:def_10 ::_thesis: 0 is UpperBound of A
 -infty is UpperBound of A by A3, Def3;
hence  0 is UpperBound of A by Th71; ::_thesis: verum
end;
suppose sup A in REAL ; ::_thesis: A is bounded_above
then reconsider r = sup A as real number ;
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of A
thus  r is UpperBound of A by Def3; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:74
for A being ext-real-membered set holds
( A is bounded_below iff inf A <> -infty )
proof
let A be ext-real-membered set ; ::_thesis: ( A is bounded_below iff inf A <> -infty )
hereby  ::_thesis: ( inf A <> -infty implies A is bounded_below )
assume A1: A is bounded_below ; ::_thesis: inf A <> -infty
percases ( A = {} or A = {+infty} or inf A in REAL ) by A1, Th58;
suppose A = {} ; ::_thesis: inf A <> -infty
hence  inf A <> -infty by Th38; ::_thesis: verum
end;
suppose A = {+infty} ; ::_thesis: inf A <> -infty
hence  inf A <> -infty by Lm2; ::_thesis: verum
end;
suppose inf A in REAL ; ::_thesis: inf A <> -infty
hence  inf A <> -infty ; ::_thesis: verum
end;
end;
end;
assume A2: inf A <> -infty ; ::_thesis: A is bounded_below
percases ( inf A = +infty or inf A in REAL ) by A2, XXREAL_0:14;
supposeA3: inf A = +infty ; ::_thesis: A is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of A
 +infty is LowerBound of A by A3, Def4;
hence  0 is LowerBound of A by Th72; ::_thesis: verum
end;
suppose inf A in REAL ; ::_thesis: A is bounded_below
then reconsider r = inf A as real number ;
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of A
thus  r is LowerBound of A by Def4; ::_thesis: verum
end;
end;
end;

begin

definition
let A be ext-real-membered set ;
attrA is interval  means :Def12: :: XXREAL_2:def 12
 for r, s being ext-real number st r in A & s in A holds
[.r,s.] c= A;
end;

:: deftheorem Def12 defines interval XXREAL_2:def_12_:_
 for A being ext-real-membered set holds
( A is interval iff for r, s being ext-real number st r in A & s in A holds
[.r,s.] c= A );

registration
cluster ExtREAL  ->  interval ;
coherence
 ExtREAL is interval
proof
let r be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st r in ExtREAL & s in ExtREAL holds
[.r,s.] c= ExtREAL
let s be ext-real number ; ::_thesis: ( r in ExtREAL & s in ExtREAL implies [.r,s.] c= ExtREAL )
thus  ( r in ExtREAL & s in ExtREAL implies [.r,s.] c= ExtREAL ) by MEMBERED:2; ::_thesis: verum
end;
cluster ext-real-membered empty  ->  ext-real-membered interval for set ;
coherence
 for b1 being ext-real-membered set st b1 is empty holds
b1 is interval
proof
let A be ext-real-membered set ; ::_thesis: ( A is empty implies A is interval )
assume A1: A is empty ; ::_thesis: A is interval
let r be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st r in A & s in A holds
[.r,s.] c= A
let s be ext-real number ; ::_thesis: ( r in A & s in A implies [.r,s.] c= A )
thus  ( r in A & s in A implies [.r,s.] c= A ) by A1; ::_thesis: verum
end;
let r, s be ext-real number ;
cluster[.r,s.] ->  interval ;
coherence
 [.r,s.] is interval
proof
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in [.r,s.] & s in [.r,s.] holds
[.x,s.] c= [.r,s.]
let y be ext-real number ; ::_thesis: ( x in [.r,s.] & y in [.r,s.] implies [.x,y.] c= [.r,s.] )
assume  x in [.r,s.] ; ::_thesis: ( not y in [.r,s.] or [.x,y.] c= [.r,s.] )
then A2: r <= x by XXREAL_1:1;
assume  y in [.r,s.] ; ::_thesis: [.x,y.] c= [.r,s.]
then A3: y <= s by XXREAL_1:1;
let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in [.x,y.] or z in [.r,s.] )
assume A4: z in [.x,y.] ; ::_thesis: z in [.r,s.]
then  x <= z by XXREAL_1:1;
then A5: r <= z by A2, XXREAL_0:2;
 z <= y by A4, XXREAL_1:1;
then  z <= s by A3, XXREAL_0:2;
hence  z in [.r,s.] by A5, XXREAL_1:1; ::_thesis: verum
end;
cluster].r,s.] ->  interval ;
coherence
 ].r,s.] is interval
proof
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in ].r,s.] & s in ].r,s.] holds
[.x,s.] c= ].r,s.]
let y be ext-real number ; ::_thesis: ( x in ].r,s.] & y in ].r,s.] implies [.x,y.] c= ].r,s.] )
assume  x in ].r,s.] ; ::_thesis: ( not y in ].r,s.] or [.x,y.] c= ].r,s.] )
then A6: r < x by XXREAL_1:2;
assume  y in ].r,s.] ; ::_thesis: [.x,y.] c= ].r,s.]
then A7: y <= s by XXREAL_1:2;
let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in [.x,y.] or z in ].r,s.] )
assume A8: z in [.x,y.] ; ::_thesis: z in ].r,s.]
then  x <= z by XXREAL_1:1;
then A9: r < z by A6, XXREAL_0:2;
 z <= y by A8, XXREAL_1:1;
then  z <= s by A7, XXREAL_0:2;
hence  z in ].r,s.] by A9, XXREAL_1:2; ::_thesis: verum
end;
cluster[.r,s.[ ->  interval ;
coherence
 [.r,s.[ is interval
proof
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in [.r,s.[ & s in [.r,s.[ holds
[.x,s.] c= [.r,s.[
let y be ext-real number ; ::_thesis: ( x in [.r,s.[ & y in [.r,s.[ implies [.x,y.] c= [.r,s.[ )
assume  x in [.r,s.[ ; ::_thesis: ( not y in [.r,s.[ or [.x,y.] c= [.r,s.[ )
then A10: r <= x by XXREAL_1:3;
assume  y in [.r,s.[ ; ::_thesis: [.x,y.] c= [.r,s.[
then A11: y < s by XXREAL_1:3;
let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in [.x,y.] or z in [.r,s.[ )
assume A12: z in [.x,y.] ; ::_thesis: z in [.r,s.[
then  x <= z by XXREAL_1:1;
then A13: r <= z by A10, XXREAL_0:2;
 z <= y by A12, XXREAL_1:1;
then  z < s by A11, XXREAL_0:2;
hence  z in [.r,s.[ by A13, XXREAL_1:3; ::_thesis: verum
end;
cluster].r,s.[ ->  interval ;
coherence
 ].r,s.[ is interval
proof
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in ].r,s.[ & s in ].r,s.[ holds
[.x,s.] c= ].r,s.[
let y be ext-real number ; ::_thesis: ( x in ].r,s.[ & y in ].r,s.[ implies [.x,y.] c= ].r,s.[ )
assume  x in ].r,s.[ ; ::_thesis: ( not y in ].r,s.[ or [.x,y.] c= ].r,s.[ )
then A14: r < x by XXREAL_1:4;
assume  y in ].r,s.[ ; ::_thesis: [.x,y.] c= ].r,s.[
then A15: y < s by XXREAL_1:4;
let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in [.x,y.] or z in ].r,s.[ )
assume A16: z in [.x,y.] ; ::_thesis: z in ].r,s.[
then  x <= z by XXREAL_1:1;
then A17: r < z by A14, XXREAL_0:2;
 z <= y by A16, XXREAL_1:1;
then  z < s by A15, XXREAL_0:2;
hence  z in ].r,s.[ by A17, XXREAL_1:4; ::_thesis: verum
end;
end;

registration
cluster REAL  ->  interval ;
coherence
 REAL is interval by XXREAL_1:224;
end;

registration
cluster ext-real-membered non empty interval for set ;
existence
 ex b1 being ext-real-membered non empty set st b1 is interval
proof
take  REAL ; ::_thesis: REAL is interval
thus  REAL is interval ; ::_thesis: verum
end;
end;

registration
let A, B be ext-real-membered interval set ;
clusterA /\ B ->  interval ;
coherence
 A /\ B is interval
proof
let r, s be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: ( r in A /\ B & s in A /\ B implies [.r,s.] c= A /\ B )
assume that
A1: r in A /\ B and
A2: s in A /\ B ; ::_thesis: [.r,s.] c= A /\ B
A3: s in B by A2, XBOOLE_0:def_4;
 r in B by A1, XBOOLE_0:def_4;
then A4: [.r,s.] c= B by A3, Def12;
A5: s in A by A2, XBOOLE_0:def_4;
 r in A by A1, XBOOLE_0:def_4;
then  [.r,s.] c= A by A5, Def12;
hence  [.r,s.] c= A /\ B by A4, XBOOLE_1:19; ::_thesis: verum
end;
end;


registration
let r, s be ext-real number ;
cluster].r,s.] ->  non left_end ;
coherence
 not ].r,s.] is left_end
proof
assume  ].r,s.] is left_end ; ::_thesis: contradiction
then A1: inf ].r,s.] in ].r,s.] by Def5;
then A2: inf ].r,s.] <= s by XXREAL_1:2;
 r < inf ].r,s.] by A1, XXREAL_1:2;
then  r < s by A2, XXREAL_0:2;
then  r = inf ].r,s.] by Th27;
hence  contradiction by A1, XXREAL_1:2; ::_thesis: verum
end;
cluster[.r,s.[ ->  non right_end ;
coherence
 not [.r,s.[ is right_end
proof
assume  [.r,s.[ is right_end ; ::_thesis: contradiction
then A3: sup [.r,s.[ in [.r,s.[ by Def6;
then A4: sup [.r,s.[ < s by XXREAL_1:3;
 r <= sup [.r,s.[ by A3, XXREAL_1:3;
then  r < s by A4, XXREAL_0:2;
then  s = sup [.r,s.[ by Th31;
hence  contradiction by A3, XXREAL_1:3; ::_thesis: verum
end;
cluster].r,s.[ ->  non left_end non right_end ;
coherence
 ( not ].r,s.[ is left_end & not ].r,s.[ is right_end )
proof
thus  not ].r,s.[ is left_end ::_thesis: not ].r,s.[ is right_end
proof
assume  ].r,s.[ is left_end ; ::_thesis: contradiction
then A5: inf ].r,s.[ in ].r,s.[ by Def5;
then A6: inf ].r,s.[ < s by XXREAL_1:4;
 r < inf ].r,s.[ by A5, XXREAL_1:4;
then  r < s by A6, XXREAL_0:2;
then  r = inf ].r,s.[ by Th28;
hence  contradiction by A5, XXREAL_1:4; ::_thesis: verum
end;
assume  ].r,s.[ is right_end ; ::_thesis: contradiction
then A7: sup ].r,s.[ in ].r,s.[ by Def6;
then A8: sup ].r,s.[ < s by XXREAL_1:4;
 r < sup ].r,s.[ by A7, XXREAL_1:4;
then  r < s by A8, XXREAL_0:2;
then  s = sup ].r,s.[ by Th32;
hence  contradiction by A7, XXREAL_1:4; ::_thesis: verum
end;
end;

registration
cluster ext-real-membered left_end right_end interval for set ;
existence
 ex b1 being ext-real-membered set st
( b1 is left_end & b1 is right_end & b1 is interval )
proof
take  [.0,1.] ; ::_thesis: ( [.0,1.] is left_end & [.0,1.] is right_end & [.0,1.] is interval )
thus  ( [.0,1.] is left_end & [.0,1.] is right_end & [.0,1.] is interval ) by Th33; ::_thesis: verum
end;
cluster ext-real-membered non left_end right_end interval for set ;
existence
 ex b1 being ext-real-membered set st
( not b1 is left_end & b1 is right_end & b1 is interval )
proof
take  ].0,1.] ; ::_thesis: ( not ].0,1.] is left_end & ].0,1.] is right_end & ].0,1.] is interval )
thus  ( not ].0,1.] is left_end & ].0,1.] is right_end & ].0,1.] is interval ) by Th35; ::_thesis: verum
end;
cluster ext-real-membered left_end non right_end interval for set ;
existence
 ex b1 being ext-real-membered set st
( b1 is left_end & not b1 is right_end & b1 is interval )
proof
take  [.0,1.[ ; ::_thesis: ( [.0,1.[ is left_end & not [.0,1.[ is right_end & [.0,1.[ is interval )
thus  ( [.0,1.[ is left_end & not [.0,1.[ is right_end & [.0,1.[ is interval ) by Th34; ::_thesis: verum
end;
cluster ext-real-membered non empty non left_end non right_end interval for set ;
existence
 ex b1 being ext-real-membered set st
( not b1 is left_end & not b1 is right_end & b1 is interval & not b1 is empty )
proof
take  ].0,2.[ ; ::_thesis: ( not ].0,2.[ is left_end & not ].0,2.[ is right_end & ].0,2.[ is interval & not ].0,2.[ is empty )
 1 in ].0,2.[ by XXREAL_1:4;
hence  ( not ].0,2.[ is left_end & not ].0,2.[ is right_end & ].0,2.[ is interval & not ].0,2.[ is empty ) ; ::_thesis: verum
end;
end;

theorem :: XXREAL_2:75
for A being ext-real-membered left_end right_end interval set holds A = [.(min A),(max A).]
proof
let A be ext-real-membered left_end right_end interval set ; ::_thesis: A = [.(min A),(max A).]
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in A or x in [.(min A),(max A).] ) & ( not x in [.(min A),(max A).] or x in A ) )
A1: max A in A by Def6;
thus  ( x in A implies x in [.(min A),(max A).] ) ::_thesis: ( not x in [.(min A),(max A).] or x in A )
proof
assume A2: x in A ; ::_thesis: x in [.(min A),(max A).]
then A3: x <= max A by Th4;
 min A <= x by A2, Th3;
hence  x in [.(min A),(max A).] by A3, XXREAL_1:1; ::_thesis: verum
end;
 min A in A by Def5;
then  [.(min A),(max A).] c= A by A1, Def12;
hence  ( not x in [.(min A),(max A).] or x in A ) ; ::_thesis: verum
end;

theorem :: XXREAL_2:76
for A being ext-real-membered non left_end right_end interval set holds A = ].(inf A),(max A).]
proof
let A be ext-real-membered non left_end right_end interval set ; ::_thesis: A = ].(inf A),(max A).]
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in A or x in ].(inf A),(max A).] ) & ( not x in ].(inf A),(max A).] or x in A ) )
defpred S1[ ext-real number ] means ( $1 in A & $1 < x );
thus  ( x in A implies x in ].(inf A),(max A).] ) ::_thesis: ( not x in ].(inf A),(max A).] or x in A )
proof
A1: not inf A in A by Def5;
assume A2: x in A ; ::_thesis: x in ].(inf A),(max A).]
then A3: x <= max A by Th4;
 inf A <= x by A2, Th3;
then  inf A < x by A2, A1, XXREAL_0:1;
hence  x in ].(inf A),(max A).] by A3, XXREAL_1:2; ::_thesis: verum
end;
assume A4: x in ].(inf A),(max A).] ; ::_thesis: x in A
percases ( for r being ext-real number holds not S1[r] or ex r being ext-real number st S1[r] ) ;
suppose for r being ext-real number holds not S1[r] ; ::_thesis: x in A
then  x is LowerBound of A by Def2;
then  x <= inf A by Def4;
hence  x in A by A4, XXREAL_1:2; ::_thesis: verum
end;
suppose ex r being ext-real number st S1[r] ; ::_thesis: x in A
then consider r being ext-real number  such that
A5: r in A and
A6: r < x ;
 x <= max A by A4, XXREAL_1:2;
then A7: x in [.r,(max A).] by A6, XXREAL_1:1;
 max A in A by Def6;
then  [.r,(max A).] c= A by A5, Def12;
hence  x in A by A7; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:77
for A being ext-real-membered left_end non right_end interval set holds A = [.(min A),(sup A).[
proof
let A be ext-real-membered left_end non right_end interval set ; ::_thesis: A = [.(min A),(sup A).[
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in A or x in [.(min A),(sup A).[ ) & ( not x in [.(min A),(sup A).[ or x in A ) )
defpred S1[ ext-real number ] means ( $1 in A & $1 > x );
thus  ( x in A implies x in [.(min A),(sup A).[ ) ::_thesis: ( not x in [.(min A),(sup A).[ or x in A )
proof
A1: not sup A in A by Def6;
assume A2: x in A ; ::_thesis: x in [.(min A),(sup A).[
then A3: min A <= x by Th3;
 x <= sup A by A2, Th4;
then  x < sup A by A2, A1, XXREAL_0:1;
hence  x in [.(min A),(sup A).[ by A3, XXREAL_1:3; ::_thesis: verum
end;
assume A4: x in [.(min A),(sup A).[ ; ::_thesis: x in A
percases ( for r being ext-real number holds not S1[r] or ex r being ext-real number st S1[r] ) ;
suppose for r being ext-real number holds not S1[r] ; ::_thesis: x in A
then  x is UpperBound of A by Def1;
then  sup A <= x by Def3;
hence  x in A by A4, XXREAL_1:3; ::_thesis: verum
end;
suppose ex r being ext-real number st S1[r] ; ::_thesis: x in A
then consider r being ext-real number  such that
A5: r in A and
A6: r > x ;
 inf A <= x by A4, XXREAL_1:3;
then A7: x in [.(inf A),r.] by A6, XXREAL_1:1;
 min A in A by Def5;
then  [.(inf A),r.] c= A by A5, Def12;
hence  x in A by A7; ::_thesis: verum
end;
end;
end;

theorem Th78: :: XXREAL_2:78
for A being ext-real-membered non empty non left_end non right_end interval set holds A = ].(inf A),(sup A).[
proof
let A be ext-real-membered non empty non left_end non right_end interval set ; ::_thesis: A = ].(inf A),(sup A).[
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in A or x in ].(inf A),(sup A).[ ) & ( not x in ].(inf A),(sup A).[ or x in A ) )
defpred S1[ ext-real number ] means ( $1 in A & $1 < x );
defpred S2[ ext-real number ] means ( $1 in A & $1 > x );
thus  ( x in A implies x in ].(inf A),(sup A).[ ) ::_thesis: ( not x in ].(inf A),(sup A).[ or x in A )
proof
assume A1: x in A ; ::_thesis: x in ].(inf A),(sup A).[
then A2: x <> sup A by Def6;
 x <= sup A by A1, Th4;
then A3: x < sup A by A2, XXREAL_0:1;
A4: x <> inf A by A1, Def5;
 inf A <= x by A1, Th3;
then  inf A < x by A4, XXREAL_0:1;
hence  x in ].(inf A),(sup A).[ by A3, XXREAL_1:4; ::_thesis: verum
end;
assume A5: x in ].(inf A),(sup A).[ ; ::_thesis: x in A
percases ( for r being ext-real number holds not S1[r] or for r being ext-real number holds not S2[r] or ( ex r being ext-real number st S1[r] & ex r being ext-real number st S2[r] ) ) ;
suppose for r being ext-real number holds not S1[r] ; ::_thesis: x in A
then  x is LowerBound of A by Def2;
then  x <= inf A by Def4;
hence  x in A by A5, XXREAL_1:4; ::_thesis: verum
end;
suppose for r being ext-real number holds not S2[r] ; ::_thesis: x in A
then  x is UpperBound of A by Def1;
then  sup A <= x by Def3;
hence  x in A by A5, XXREAL_1:4; ::_thesis: verum
end;
supposethat A6: ex r being ext-real number st S1[r] and
A7: ex r being ext-real number st S2[r] ; ::_thesis: x in A
consider r being ext-real number  such that
A8: r in A and
A9: r < x by A6;
consider s being ext-real number  such that
A10: s in A and
A11: s > x by A7;
A12: x in [.r,s.] by A9, A11, XXREAL_1:1;
 [.r,s.] c= A by A8, A10, Def12;
hence  x in A by A12; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:79
for A being ext-real-membered non left_end non right_end interval set ex r, s being ext-real number st
( r <= s & A = ].r,s.[ )
proof
let A be ext-real-membered non left_end non right_end interval set ; ::_thesis: ex r, s being ext-real number st
( r <= s & A = ].r,s.[ )
percases ( A is empty or not A is empty ) ;
supposeA1: A is empty ; ::_thesis: ex r, s being ext-real number st
( r <= s & A = ].r,s.[ )
take  -infty ; ::_thesis: ex s being ext-real number st
( -infty <= s & A = ].-infty,s.[ )
take  -infty ; ::_thesis: ( -infty <= -infty & A = ].-infty,-infty.[ )
thus  ( -infty <= -infty & A = ].-infty,-infty.[ ) by A1; ::_thesis: verum
end;
supposeA2: not A is empty ; ::_thesis: ex r, s being ext-real number st
( r <= s & A = ].r,s.[ )
take  inf A ; ::_thesis: ex s being ext-real number st
( inf A <= s & A = ].(inf A),s.[ )
take  sup A ; ::_thesis: ( inf A <= sup A & A = ].(inf A),(sup A).[ )
thus  inf A <= sup A by A2, Th40; ::_thesis: A = ].(inf A),(sup A).[
thus  A = ].(inf A),(sup A).[ by A2, Th78; ::_thesis: verum
end;
end;
end;

theorem Th80: :: XXREAL_2:80
for A being ext-real-membered set st A is interval holds
for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A
proof
let A be ext-real-membered set ; ::_thesis: ( A is interval implies for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A )
assume A1: A is interval ; ::_thesis: for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A
let x, y, r be ext-real number ; ::_thesis: ( x in A & y in A & x <= r & r <= y implies r in A )
assume that
A2: x in A and
A3: y in A and
A4: x <= r and
A5: r <= y ; ::_thesis: r in A
A6: r in [.x,y.] by A4, A5, XXREAL_1:1;
 [.x,y.] c= A by A1, A2, A3, Def12;
hence  r in A by A6; ::_thesis: verum
end;

theorem Th81: :: XXREAL_2:81
for A being ext-real-membered set st A is interval holds
for x, r being ext-real number st x in A & x <= r & r < sup A holds
r in A
proof
let A be ext-real-membered set ; ::_thesis: ( A is interval implies for x, r being ext-real number st x in A & x <= r & r < sup A holds
r in A )
assume A1: A is interval ; ::_thesis: for x, r being ext-real number st x in A & x <= r & r < sup A holds
r in A
let x, r be ext-real number ; ::_thesis: ( x in A & x <= r & r < sup A implies r in A )
assume that
A2: x in A and
A3: x <= r and
A4: r < sup A ; ::_thesis: r in A
percases ( ex y being ext-real number st
( y in A & r < y ) or for y being ext-real number holds
( not y in A or not r < y ) ) ;
suppose ex y being ext-real number st
( y in A & r < y ) ; ::_thesis: r in A
hence  r in A by A1, A2, A3, Th80; ::_thesis: verum
end;
suppose for y being ext-real number holds
( not y in A or not r < y ) ; ::_thesis: r in A
then  r is UpperBound of A by Def1;
hence  r in A by A4, Def3; ::_thesis: verum
end;
end;
end;

theorem Th82: :: XXREAL_2:82
for A being ext-real-membered set st A is interval holds
for x, r being ext-real number st x in A & inf A < r & r <= x holds
r in A
proof
let A be ext-real-membered set ; ::_thesis: ( A is interval implies for x, r being ext-real number st x in A & inf A < r & r <= x holds
r in A )
assume A1: A is interval ; ::_thesis: for x, r being ext-real number st x in A & inf A < r & r <= x holds
r in A
let x, r be ext-real number ; ::_thesis: ( x in A & inf A < r & r <= x implies r in A )
assume that
A2: x in A and
A3: inf A < r and
A4: r <= x ; ::_thesis: r in A
percases ( ex y being ext-real number st
( y in A & r > y ) or for y being ext-real number holds
( not y in A or not r > y ) ) ;
suppose ex y being ext-real number st
( y in A & r > y ) ; ::_thesis: r in A
hence  r in A by A1, A2, A4, Th80; ::_thesis: verum
end;
suppose for y being ext-real number holds
( not y in A or not r > y ) ; ::_thesis: r in A
then  r is LowerBound of A by Def2;
hence  r in A by A3, Def4; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:83
for A being ext-real-membered set st A is interval holds
for r being ext-real number st inf A < r & r < sup A holds
r in A
proof
let A be ext-real-membered set ; ::_thesis: ( A is interval implies for r being ext-real number st inf A < r & r < sup A holds
r in A )
assume A1: A is interval ; ::_thesis: for r being ext-real number st inf A < r & r < sup A holds
r in A
let r be ext-real number ; ::_thesis: ( inf A < r & r < sup A implies r in A )
assume that
A2: inf A < r and
A3: r < sup A ; ::_thesis: r in A
percases ( ex y being ext-real number st
( y in A & r > y ) or for y being ext-real number holds
( not y in A or not r > y ) ) ;
suppose ex y being ext-real number st
( y in A & r > y ) ; ::_thesis: r in A
hence  r in A by A1, A3, Th81; ::_thesis: verum
end;
suppose for y being ext-real number holds
( not y in A or not r > y ) ; ::_thesis: r in A
then  r is LowerBound of A by Def2;
hence  r in A by A2, Def4; ::_thesis: verum
end;
end;
end;

theorem Th84: :: XXREAL_2:84
for A being ext-real-membered set st ( for x, y, r being ext-real number st x in A & y in A & x < r & r < y holds
r in A ) holds
A is interval
proof
let A be ext-real-membered set ; ::_thesis: ( ( for x, y, r being ext-real number st x in A & y in A & x < r & r < y holds
r in A ) implies A is interval )
assume A1: for x, y, r being ext-real number st x in A & y in A & x < r & r < y holds
r in A ; ::_thesis: A is interval
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in A & s in A holds
[.x,s.] c= A
let y be ext-real number ; ::_thesis: ( x in A & y in A implies [.x,y.] c= A )
assume that
A2: x in A and
A3: y in A ; ::_thesis: [.x,y.] c= A
let r be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not r in [.x,y.] or r in A )
assume  r in [.x,y.] ; ::_thesis: r in A
then  r in ].x,y.[ \/ {x,y} by XXREAL_1:29, XXREAL_1:128;
then A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def_3;
percases ( r = x or r = y or r in ].x,y.[ ) by A4, TARSKI:def_2;
suppose r = x ; ::_thesis: r in A
hence  r in A by A2; ::_thesis: verum
end;
suppose r = y ; ::_thesis: r in A
hence  r in A by A3; ::_thesis: verum
end;
supposeA5: r in ].x,y.[ ; ::_thesis: r in A
then A6: r < y by XXREAL_1:4;
 x < r by A5, XXREAL_1:4;
hence  r in A by A1, A2, A3, A6; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:85
for A being ext-real-membered set st ( for x, r being ext-real number st x in A & x < r & r < sup A holds
r in A ) holds
A is interval
proof
let A be ext-real-membered set ; ::_thesis: ( ( for x, r being ext-real number st x in A & x < r & r < sup A holds
r in A ) implies A is interval )
assume A1: for x, r being ext-real number st x in A & x < r & r < sup A holds
r in A ; ::_thesis: A is interval
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in A & s in A holds
[.x,s.] c= A
let y be ext-real number ; ::_thesis: ( x in A & y in A implies [.x,y.] c= A )
assume that
A2: x in A and
A3: y in A ; ::_thesis: [.x,y.] c= A
let r be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not r in [.x,y.] or r in A )
assume  r in [.x,y.] ; ::_thesis: r in A
then  r in ].x,y.[ \/ {x,y} by XXREAL_1:29, XXREAL_1:128;
then A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def_3;
percases ( r = x or r = y or r in ].x,y.[ ) by A4, TARSKI:def_2;
suppose r = x ; ::_thesis: r in A
hence  r in A by A2; ::_thesis: verum
end;
suppose r = y ; ::_thesis: r in A
hence  r in A by A3; ::_thesis: verum
end;
supposeA5: r in ].x,y.[ ; ::_thesis: r in A
then A6: r < y by XXREAL_1:4;
 y <= sup A by A3, Th4;
then A7: r < sup A by A6, XXREAL_0:2;
 x < r by A5, XXREAL_1:4;
hence  r in A by A1, A2, A7; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:86
for A being ext-real-membered set st ( for y, r being ext-real number st y in A & inf A < r & r < y holds
r in A ) holds
A is interval
proof
let A be ext-real-membered set ; ::_thesis: ( ( for y, r being ext-real number st y in A & inf A < r & r < y holds
r in A ) implies A is interval )
assume A1: for y, r being ext-real number st y in A & inf A < r & r < y holds
r in A ; ::_thesis: A is interval
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in A & s in A holds
[.x,s.] c= A
let y be ext-real number ; ::_thesis: ( x in A & y in A implies [.x,y.] c= A )
assume that
A2: x in A and
A3: y in A ; ::_thesis: [.x,y.] c= A
let r be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not r in [.x,y.] or r in A )
assume  r in [.x,y.] ; ::_thesis: r in A
then  r in ].x,y.[ \/ {x,y} by XXREAL_1:29, XXREAL_1:128;
then A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def_3;
percases ( r = x or r = y or r in ].x,y.[ ) by A4, TARSKI:def_2;
suppose r = x ; ::_thesis: r in A
hence  r in A by A2; ::_thesis: verum
end;
suppose r = y ; ::_thesis: r in A
hence  r in A by A3; ::_thesis: verum
end;
supposeA5: r in ].x,y.[ ; ::_thesis: r in A
then A6: x < r by XXREAL_1:4;
 inf A <= x by A2, Th3;
then A7: inf A < r by A6, XXREAL_0:2;
 r < y by A5, XXREAL_1:4;
hence  r in A by A1, A3, A7; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_2:87
for A being ext-real-membered set st ( for r being ext-real number st inf A < r & r < sup A holds
r in A ) holds
A is interval
proof
let A be ext-real-membered set ; ::_thesis: ( ( for r being ext-real number st inf A < r & r < sup A holds
r in A ) implies A is interval )
assume A1: for r being ext-real number st inf A < r & r < sup A holds
r in A ; ::_thesis: A is interval
let x be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: for s being ext-real number st x in A & s in A holds
[.x,s.] c= A
let y be ext-real number ; ::_thesis: ( x in A & y in A implies [.x,y.] c= A )
assume that
A2: x in A and
A3: y in A ; ::_thesis: [.x,y.] c= A
let r be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not r in [.x,y.] or r in A )
assume  r in [.x,y.] ; ::_thesis: r in A
then  r in ].x,y.[ \/ {x,y} by XXREAL_1:29, XXREAL_1:128;
then A4: ( r in ].x,y.[ or r in {x,y} ) by XBOOLE_0:def_3;
percases ( r = x or r = y or r in ].x,y.[ ) by A4, TARSKI:def_2;
suppose r = x ; ::_thesis: r in A
hence  r in A by A2; ::_thesis: verum
end;
suppose r = y ; ::_thesis: r in A
hence  r in A by A3; ::_thesis: verum
end;
supposeA5: r in ].x,y.[ ; ::_thesis: r in A
then A6: r < y by XXREAL_1:4;
 y <= sup A by A3, Th4;
then A7: r < sup A by A6, XXREAL_0:2;
A8: x < r by A5, XXREAL_1:4;
 inf A <= x by A2, Th3;
then  inf A < r by A8, XXREAL_0:2;
hence  r in A by A1, A7; ::_thesis: verum
end;
end;
end;

theorem Th88: :: XXREAL_2:88
for A being ext-real-membered set st ( for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A ) holds
A is interval
proof
let A be ext-real-membered set ; ::_thesis: ( ( for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A ) implies A is interval )
assume  for x, y, r being ext-real number st x in A & y in A & x <= r & r <= y holds
r in A ; ::_thesis: A is interval
then  for x, y, r being ext-real number st x in A & y in A & x < r & r < y holds
r in A ;
hence  A is interval by Th84; ::_thesis: verum
end;

theorem :: XXREAL_2:89
for A, B being ext-real-membered set st A is interval & B is interval & A meets B holds
A \/ B is interval
proof
let A, B be ext-real-membered set ; ::_thesis: ( A is interval & B is interval & A meets B implies A \/ B is interval )
assume that
A1: A is interval and
A2: B is interval ; ::_thesis: ( not A meets B or A \/ B is interval )
given z being ext-real number  such that A3: z in A and
A4: z in B ; :: according to MEMBERED:def_20 ::_thesis: A \/ B is interval
 for x, y, r being ext-real number st x in A \/ B & y in A \/ B & x <= r & r <= y holds
r in A \/ B
proof
let x, y, r be ext-real number ; ::_thesis: ( x in A \/ B & y in A \/ B & x <= r & r <= y implies r in A \/ B )
assume that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x <= r and
A8: r <= y ; ::_thesis: r in A \/ B
percases ( ( x in A & y in A ) or ( x in A & y in B ) or ( x in B & y in A ) or ( x in B & y in B ) ) by A5, A6, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: r in A \/ B
then  r in A by A1, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A9: x in A and
A10: y in B ; ::_thesis: r in A \/ B
percases ( r <= z or z <= r ) ;
suppose r <= z ; ::_thesis: r in A \/ B
then  r in A by A1, A3, A7, A9, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose z <= r ; ::_thesis: r in A \/ B
then  r in B by A2, A4, A8, A10, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
supposethat A11: x in B and
A12: y in A ; ::_thesis: r in A \/ B
percases ( z <= r or r <= z ) ;
suppose z <= r ; ::_thesis: r in A \/ B
then  r in A by A1, A3, A8, A12, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose r <= z ; ::_thesis: r in A \/ B
then  r in B by A2, A4, A7, A11, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
suppose ( x in B & y in B ) ; ::_thesis: r in A \/ B
then  r in B by A2, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  A \/ B is interval by Th88; ::_thesis: verum
end;

theorem :: XXREAL_2:90
for A, B being ext-real-membered set st A is interval & B is left_end & B is interval & sup A = inf B holds
A \/ B is interval
proof
let A, B be ext-real-membered set ; ::_thesis: ( A is interval & B is left_end & B is interval & sup A = inf B implies A \/ B is interval )
assume that
A1: A is interval and
A2: ( B is left_end & B is interval ) and
A3: sup A = inf B ; ::_thesis: A \/ B is interval
set z = inf B;
A4: inf B in B by A2, Def5;
 for x, y, r being ext-real number st x in A \/ B & y in A \/ B & x < r & r < y holds
r in A \/ B
proof
let x, y, r be ext-real number ; ::_thesis: ( x in A \/ B & y in A \/ B & x < r & r < y implies r in A \/ B )
assume that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x < r and
A8: r < y ; ::_thesis: r in A \/ B
percases ( ( x in A & y in A ) or ( x in A & y in B ) or ( x in B & y in A ) or ( x in B & y in B ) ) by A5, A6, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: r in A \/ B
then  r in A by A1, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A9: x in A and
A10: y in B ; ::_thesis: r in A \/ B
percases ( r < inf B or inf B <= r ) ;
suppose r < inf B ; ::_thesis: r in A \/ B
then  r in A by A1, A3, A7, A9, Th81;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose inf B <= r ; ::_thesis: r in A \/ B
then  r in B by A2, A4, A8, A10, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
supposethat A11: x in B and
A12: y in A ; ::_thesis: r in A \/ B
percases ( inf B < r or r <= inf B ) ;
supposeA13: inf B < r ; ::_thesis: r in A \/ B
 y <= inf B by A3, A12, Th4;
hence  r in A \/ B by A8, A13, XXREAL_0:2; ::_thesis: verum
end;
suppose r <= inf B ; ::_thesis: r in A \/ B
then  r in B by A2, A4, A7, A11, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
suppose ( x in B & y in B ) ; ::_thesis: r in A \/ B
then  r in B by A2, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  A \/ B is interval by Th84; ::_thesis: verum
end;

theorem :: XXREAL_2:91
for A, B being ext-real-membered set st A is right_end & A is interval & B is interval & sup A = inf B holds
A \/ B is interval
proof
let A, B be ext-real-membered set ; ::_thesis: ( A is right_end & A is interval & B is interval & sup A = inf B implies A \/ B is interval )
assume that
A1: ( A is right_end & A is interval ) and
A2: B is interval and
A3: sup A = inf B ; ::_thesis: A \/ B is interval
set z = inf B;
A4: inf B in A by A1, A3, Def6;
 for x, y, r being ext-real number st x in A \/ B & y in A \/ B & x < r & r < y holds
r in A \/ B
proof
let x, y, r be ext-real number ; ::_thesis: ( x in A \/ B & y in A \/ B & x < r & r < y implies r in A \/ B )
assume that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x < r and
A8: r < y ; ::_thesis: r in A \/ B
percases ( ( x in A & y in A ) or ( x in A & y in B ) or ( x in B & y in A ) or ( x in B & y in B ) ) by A5, A6, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: r in A \/ B
then  r in A by A1, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A9: x in A and
A10: y in B ; ::_thesis: r in A \/ B
percases ( r <= inf B or inf B < r ) ;
suppose r <= inf B ; ::_thesis: r in A \/ B
then  r in A by A1, A4, A7, A9, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose inf B < r ; ::_thesis: r in A \/ B
then  r in B by A2, A8, A10, Th82;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
supposethat A11: x in B and
A12: y in A ; ::_thesis: r in A \/ B
percases ( inf B <= r or r < inf B ) ;
suppose inf B <= r ; ::_thesis: r in A \/ B
then  r in A by A1, A4, A8, A12, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA13: r < inf B ; ::_thesis: r in A \/ B
 inf B <= x by A11, Th3;
hence  r in A \/ B by A7, A13, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
suppose ( x in B & y in B ) ; ::_thesis: r in A \/ B
then  r in B by A2, A7, A8, Th80;
hence  r in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  A \/ B is interval by Th84; ::_thesis: verum
end;

registration
cluster ext-real-membered left_end  ->  ext-real-membered non empty for set ;
coherence
 for b1 being ext-real-membered set st b1 is left_end holds
not b1 is empty
proof
let A be ext-real-membered set ; ::_thesis: ( A is left_end implies not A is empty )
assume  inf A in A ; :: according to XXREAL_2:def_5 ::_thesis: not A is empty
hence  not A is empty ; ::_thesis: verum
end;
cluster ext-real-membered right_end  ->  ext-real-membered non empty for set ;
coherence
 for b1 being ext-real-membered set st b1 is right_end holds
not b1 is empty
proof
let A be ext-real-membered set ; ::_thesis: ( A is right_end implies not A is empty )
assume  sup A in A ; :: according to XXREAL_2:def_6 ::_thesis: not A is empty
hence  not A is empty ; ::_thesis: verum
end;
end;

theorem :: XXREAL_2:92
for A being non empty Subset of ExtREAL st ( for r being Element of ExtREAL st r in A holds
r <= -infty ) holds
A = {-infty}
proof
let A be non empty Subset of ExtREAL; ::_thesis: ( ( for r being Element of ExtREAL st r in A holds
r <= -infty ) implies A = {-infty} )
assume A1: for r being Element of ExtREAL st r in A holds
r <= -infty ; ::_thesis: A = {-infty}
assume  A <> {-infty} ; ::_thesis: contradiction
then  ex a being Element of A st a <> -infty by SETFAM_1:49;
hence  contradiction by A1, XXREAL_0:6; ::_thesis: verum
end;

theorem :: XXREAL_2:93
for A being non empty Subset of ExtREAL st ( for r being Element of ExtREAL st r in A holds
+infty <= r ) holds
A = {+infty}
proof
let A be non empty Subset of ExtREAL; ::_thesis: ( ( for r being Element of ExtREAL st r in A holds
+infty <= r ) implies A = {+infty} )
assume A1: for r being Element of ExtREAL st r in A holds
+infty <= r ; ::_thesis: A = {+infty}
assume  A <> {+infty} ; ::_thesis: contradiction
then  ex a being Element of A st a <> +infty by SETFAM_1:49;
hence  contradiction by A1, XXREAL_0:4; ::_thesis: verum
end;

theorem Th94: :: XXREAL_2:94
for A being non empty Subset of ExtREAL
for r being ext-real number st r < sup A holds
ex s being Element of ExtREAL st
( s in A & r < s )
proof
let A be non empty Subset of ExtREAL; ::_thesis: for r being ext-real number st r < sup A holds
ex s being Element of ExtREAL st
( s in A & r < s )
let r be ext-real number ; ::_thesis: ( r < sup A implies ex s being Element of ExtREAL st
( s in A & r < s ) )
assume A1: r < sup A ; ::_thesis: ex s being Element of ExtREAL st
( s in A & r < s )
assume A2: for s being Element of ExtREAL st s in A holds
not r < s ; ::_thesis: contradiction
 r is UpperBound of A
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( x in A implies x <= r )
assume  x in A ; ::_thesis: x <= r
hence  x <= r by A2; ::_thesis: verum
end;
hence  contradiction by A1, Def3; ::_thesis: verum
end;

theorem Th95: :: XXREAL_2:95
for A being non empty Subset of ExtREAL
for r being Element of ExtREAL st inf A < r holds
ex s being Element of ExtREAL st
( s in A & s < r )
proof
let A be non empty Subset of ExtREAL; ::_thesis: for r being Element of ExtREAL st inf A < r holds
ex s being Element of ExtREAL st
( s in A & s < r )
let r be Element of ExtREAL ; ::_thesis: ( inf A < r implies ex s being Element of ExtREAL st
( s in A & s < r ) )
assume A1: inf A < r ; ::_thesis: ex s being Element of ExtREAL st
( s in A & s < r )
assume A2: for s being Element of ExtREAL st s in A holds
not s < r ; ::_thesis: contradiction
 r is LowerBound of A
proof
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( x in A implies r <= x )
assume  x in A ; ::_thesis: r <= x
hence  r <= x by A2; ::_thesis: verum
end;
hence  contradiction by A1, Def4; ::_thesis: verum
end;

theorem :: XXREAL_2:96
for A, B being non empty Subset of ExtREAL st ( for r, s being Element of ExtREAL st r in A & s in B holds
r <= s ) holds
sup A <= inf B
proof
let A, B be non empty Subset of ExtREAL; ::_thesis: ( ( for r, s being Element of ExtREAL st r in A & s in B holds
r <= s ) implies sup A <= inf B )
assume A1: for r, s being Element of ExtREAL st r in A & s in B holds
r <= s ; ::_thesis: sup A <= inf B
assume  not sup A <= inf B ; ::_thesis: contradiction
then consider s1 being Element of ExtREAL  such that
A2: s1 in A and
A3: inf B < s1 by Th94;
 ex s2 being Element of ExtREAL st
( s2 in B & s2 < s1 ) by A3, Th95;
hence  contradiction by A1, A2; ::_thesis: verum
end;