:: Suprema and Infima of Intervals of Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received June 26, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


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 &amp; i <= F2() &amp; P1[i] )  }  is finite
proofend;

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
proofend;
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
proofend;
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 &amp; ( for x being UpperBound of X holds it <= x ) );
existence
 ex b1 being ext-real number st
( b1 is UpperBound of X &amp; ( for x being UpperBound of X holds b1 <= x ) )
proofend;
uniqueness
 for b1, b2 being ext-real number st b1 is UpperBound of X &amp; ( for x being UpperBound of X holds b1 <= x ) &amp; b2 is UpperBound of X &amp; ( for x being UpperBound of X holds b2 <= x ) holds
b1 = b2
proofend;
func inf X ->  ext-real number  means :Def4: :: XXREAL_2:def 4
( it is LowerBound of X &amp; ( for x being LowerBound of X holds x <= it ) );
existence
 ex b1 being ext-real number st
( b1 is LowerBound of X &amp; ( for x being LowerBound of X holds x <= b1 ) )
proofend;
uniqueness
 for b1, b2 being ext-real number st b1 is LowerBound of X &amp; ( for x being LowerBound of X holds x <= b1 ) &amp; b2 is LowerBound of X &amp; ( for x being LowerBound of X holds x <= b2 ) holds
b1 = b2
proofend;
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 &amp; ( 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 &amp; ( 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 )
proofend;

theorem Th2: :: XXREAL_2:2
for y, x being ext-real number holds
( y is LowerBound of {x} iff y <= x )
proofend;

Lm1:  for x being ext-real number holds sup {x} = x
proofend;

Lm2:  for x being ext-real number holds inf {x} = x
proofend;

registration
cluster  ->  ext-real-membered for Element of Fin ExtREAL;
coherence
 for b1 being Element of Fin ExtREAL holds b1 is ext-real-membered
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

theorem Th9: :: XXREAL_2:9
for A, B being ext-real-membered set holds inf (A \/ B) = min ((inf A),(inf B))
proofend;

theorem Th10: :: XXREAL_2:10
for A, B being ext-real-membered set holds sup (A \/ B) = max ((sup A),(sup B))
proofend;

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 &amp; b1 is right_end )
proofend;
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
proofend;
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
proofend;
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 &amp; ( 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 &amp; ( for x being ext-real number st x in X holds
b1 <= x ) ) )
proofend;
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 &amp; ( 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 &amp; ( 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 &amp; ( for x being ext-real number st x in X holds
x <= b1 ) ) )
proofend;
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 &amp; ( 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}
proofend;

Lm4:  for x, y being ext-real number
for z being UpperBound of {x,y} holds y <= z
proofend;

theorem :: XXREAL_2:12
for x, y being ext-real number holds max (x,y) = max {x,y}
proofend;

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}
proofend;

Lm6:  for x, y being ext-real number
for z being LowerBound of {x,y} holds z <= y
proofend;

theorem :: XXREAL_2:14
for x, y being ext-real number holds min {x,y} = min (x,y)
proofend;

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 &amp; b1 is finite &amp; b1 is natural-membered )
proofend;
end;

definition
let X be ext-real-membered set ;
attrX is real-bounded  means :Def11: :: XXREAL_2:def 11
( X is bounded_below &amp; 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 &amp; 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 &amp; 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 &amp; 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
proofend;
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
proofend;
end;

theorem Th15: :: XXREAL_2:15
for X being real-membered non empty set st X is bounded_below holds
inf X in REAL
proofend;

theorem Th16: :: XXREAL_2:16
for X being real-membered non empty set st X is bounded_above holds
sup X in REAL
proofend;

registration
let X be real-membered non empty bounded_above set ;
cluster sup X ->  ext-real real ;
coherence
 sup X is real
proofend;
end;

registration
let X be real-membered non empty bounded_below set ;
cluster inf X ->  ext-real real ;
coherence
 inf X is real
proofend;
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
proofend;
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
proofend;
end;

registration
cluster natural-membered  ->  natural-membered bounded_below for set ;
coherence
 for b1 being natural-membered set holds b1 is bounded_below
proofend;
end;

registration
let X be real-membered left_end set ;
cluster inf X ->  ext-real real ;
coherence
 min X is real
proofend;
end;

registration
let X be rational-membered left_end set ;
cluster inf X ->  ext-real rational ;
coherence
 min X is rational
proofend;
end;

registration
let X be integer-membered left_end set ;
cluster inf X ->  ext-real integer ;
coherence
 min X is integer
proofend;
end;

registration
let X be natural-membered left_end set ;
cluster inf X ->  ext-real natural ;
coherence
 min X is natural
proofend;
end;

registration
let X be real-membered right_end set ;
cluster sup X ->  ext-real real ;
coherence
 max X is real
proofend;
end;

registration
let X be rational-membered right_end set ;
cluster sup X ->  ext-real rational ;
coherence
 max X is rational
proofend;
end;

registration
let X be integer-membered right_end set ;
cluster sup X ->  ext-real integer ;
coherence
 max X is integer
proofend;
end;

registration
let X be natural-membered right_end set ;
cluster sup X ->  ext-real natural ;
coherence
 max X is natural
proofend;
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
proofend;
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
proofend;
end;

theorem Th17: :: XXREAL_2:17
for x, y being ext-real number holds x is LowerBound of [.x,y.]
proofend;

theorem Th18: :: XXREAL_2:18
for x, y being ext-real number holds x is LowerBound of ].x,y.]
proofend;

theorem Th19: :: XXREAL_2:19
for x, y being ext-real number holds x is LowerBound of [.x,y.[
proofend;

theorem Th20: :: XXREAL_2:20
for x, y being ext-real number holds x is LowerBound of ].x,y.[
proofend;

theorem Th21: :: XXREAL_2:21
for y, x being ext-real number holds y is UpperBound of [.x,y.]
proofend;

theorem Th22: :: XXREAL_2:22
for y, x being ext-real number holds y is UpperBound of ].x,y.]
proofend;

theorem Th23: :: XXREAL_2:23
for y, x being ext-real number holds y is UpperBound of [.x,y.[
proofend;

theorem Th24: :: XXREAL_2:24
for y, x being ext-real number holds y is UpperBound of ].x,y.[
proofend;

theorem Th25: :: XXREAL_2:25
for x, y being ext-real number st x <= y holds
inf [.x,y.] = x
proofend;

theorem Th26: :: XXREAL_2:26
for x, y being ext-real number st x < y holds
inf [.x,y.[ = x
proofend;

theorem Th27: :: XXREAL_2:27
for x, y being ext-real number st x < y holds
inf ].x,y.] = x
proofend;

theorem Th28: :: XXREAL_2:28
for x, y being ext-real number st x < y holds
inf ].x,y.[ = x
proofend;

theorem Th29: :: XXREAL_2:29
for x, y being ext-real number st x <= y holds
sup [.x,y.] = y
proofend;

theorem Th30: :: XXREAL_2:30
for x, y being ext-real number st x < y holds
sup ].x,y.] = y
proofend;

theorem Th31: :: XXREAL_2:31
for x, y being ext-real number st x < y holds
sup [.x,y.[ = y
proofend;

theorem Th32: :: XXREAL_2:32
for x, y being ext-real number st x < y holds
sup ].x,y.[ = y
proofend;

theorem Th33: :: XXREAL_2:33
for x, y being ext-real number st x <= y holds
( [.x,y.] is left_end &amp; [.x,y.] is right_end )
proofend;

theorem Th34: :: XXREAL_2:34
for x, y being ext-real number st x < y holds
[.x,y.[ is left_end
proofend;

theorem Th35: :: XXREAL_2:35
for x, y being ext-real number st x < y holds
].x,y.] is right_end
proofend;

theorem Th36: :: XXREAL_2:36
for x being ext-real number holds x is LowerBound of {}
proofend;

theorem Th37: :: XXREAL_2:37
for x being ext-real number holds x is UpperBound of {}
proofend;

theorem Th38: :: XXREAL_2:38
inf {} = +infty
proofend;

theorem Th39: :: XXREAL_2:39
sup {} = -infty
proofend;

theorem Th40: :: XXREAL_2:40
for X being ext-real-membered set holds
( not X is empty iff inf X <= sup X )
proofend;

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
proofend;
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
proofend;

theorem :: XXREAL_2:42
for X being ext-real-membered set holds -infty is LowerBound of X
proofend;

theorem Th43: :: XXREAL_2:43
for X, Y being ext-real-membered set st X c= Y &amp; Y is bounded_above holds
X is bounded_above
proofend;

theorem Th44: :: XXREAL_2:44
for X, Y being ext-real-membered set st X c= Y &amp; Y is bounded_below holds
X is bounded_below
proofend;

theorem :: XXREAL_2:45
for X, Y being ext-real-membered set st X c= Y &amp; Y is real-bounded holds
X is real-bounded
proofend;

theorem Th46: :: XXREAL_2:46
( not REAL is bounded_below &amp; not REAL is bounded_above )
proofend;

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

theorem :: XXREAL_2:47
{+infty} is bounded_below
proofend;

theorem :: XXREAL_2:48
{-infty} is bounded_above
proofend;

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
proofend;

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
proofend;

theorem Th51: :: XXREAL_2:51
for X being ext-real-membered set st -infty is UpperBound of X holds
X c= {-infty}
proofend;

theorem Th52: :: XXREAL_2:52
for X being ext-real-membered set st +infty is LowerBound of X holds
X c= {+infty}
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

theorem Th57: :: XXREAL_2:57
for X being ext-real-membered non empty set st X is bounded_above &amp; X <> {-infty} holds
sup X in REAL
proofend;

theorem Th58: :: XXREAL_2:58
for X being ext-real-membered non empty set st X is bounded_below &amp; X <> {+infty} holds
inf X in REAL
proofend;

theorem :: XXREAL_2:59
for X, Y being ext-real-membered set st X c= Y holds
sup X <= sup Y
proofend;

theorem :: XXREAL_2:60
for X, Y being ext-real-membered set st X c= Y holds
inf Y <= inf X
proofend;

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 &amp; x <= y ) holds
x <= sup X
proofend;

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 &amp; y <= x ) holds
inf X <= x
proofend;

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 &amp; x <= y ) ) holds
sup X <= sup Y
proofend;

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 &amp; x <= y ) ) holds
inf X <= inf Y
proofend;

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
proofend;

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
proofend;

theorem :: XXREAL_2:67
for X, Y being ext-real-membered set holds sup (X /\ Y) <= min ((sup X),(sup Y))
proofend;

theorem :: XXREAL_2:68
for X, Y being ext-real-membered set holds max ((inf X),(inf Y)) <= inf (X /\ Y)
proofend;

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
proofend;
end;

theorem Th69: :: XXREAL_2:69
for A being ext-real-membered set holds A c= [.(inf A),(sup A).]
proofend;

theorem :: XXREAL_2:70
for A being ext-real-membered set st sup A = inf A holds
A = {(inf A)}
proofend;

theorem Th71: :: XXREAL_2:71
for x, y being ext-real number
for A being ext-real-membered set st x <= y &amp; x is UpperBound of A holds
y is UpperBound of A
proofend;

theorem Th72: :: XXREAL_2:72
for y, x being ext-real number
for A being ext-real-membered set st y <= x &amp; x is LowerBound of A holds
y is LowerBound of A
proofend;

theorem :: XXREAL_2:73
for A being ext-real-membered set holds
( A is bounded_above iff sup A <> +infty )
proofend;

theorem :: XXREAL_2:74
for A being ext-real-membered set holds
( A is bounded_below iff inf A <> -infty )
proofend;

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 &amp; 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 &amp; s in A holds
[.r,s.] c= A );

registration
cluster ExtREAL  ->  interval ;
coherence
 ExtREAL is interval
proofend;
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
proofend;
let r, s be ext-real number ;
cluster[.r,s.] ->  interval ;
coherence
 [.r,s.] is interval
proofend;
cluster].r,s.] ->  interval ;
coherence
 ].r,s.] is interval
proofend;
cluster[.r,s.[ ->  interval ;
coherence
 [.r,s.[ is interval
proofend;
cluster].r,s.[ ->  interval ;
coherence
 ].r,s.[ is interval
proofend;
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
proofend;
end;

registration
let A, B be ext-real-membered interval set ;
clusterA /\ B ->  interval ;
coherence
 A /\ B is interval
proofend;
end;

registration
let r, s be ext-real number ;
cluster].r,s.] ->  non left_end ;
coherence
 not ].r,s.] is left_end
proofend;
cluster[.r,s.[ ->  non right_end ;
coherence
 not [.r,s.[ is right_end
proofend;
cluster].r,s.[ ->  non left_end non right_end ;
coherence
 ( not ].r,s.[ is left_end &amp; not ].r,s.[ is right_end )
proofend;
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 &amp; b1 is right_end &amp; b1 is interval )
proofend;
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 &amp; b1 is right_end &amp; b1 is interval )
proofend;
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 &amp; not b1 is right_end &amp; b1 is interval )
proofend;
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 &amp; not b1 is right_end &amp; b1 is interval &amp; not b1 is empty )
proofend;
end;

theorem :: XXREAL_2:75
for A being ext-real-membered left_end right_end interval set holds A = [.(min A),(max A).]
proofend;

theorem :: XXREAL_2:76
for A being ext-real-membered non left_end right_end interval set holds A = ].(inf A),(max A).]
proofend;

theorem :: XXREAL_2:77
for A being ext-real-membered left_end non right_end interval set holds A = [.(min A),(sup A).[
proofend;

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).[
proofend;

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 &amp; A = ].r,s.[ )
proofend;

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 &amp; y in A &amp; x <= r &amp; r <= y holds
r in A
proofend;

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 &amp; x <= r &amp; r < sup A holds
r in A
proofend;

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 &amp; inf A < r &amp; r <= x holds
r in A
proofend;

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 &amp; r < sup A holds
r in A
proofend;

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 &amp; y in A &amp; x < r &amp; r < y holds
r in A ) holds
A is interval
proofend;

theorem :: XXREAL_2:85
for A being ext-real-membered set st ( for x, r being ext-real number st x in A &amp; x < r &amp; r < sup A holds
r in A ) holds
A is interval
proofend;

theorem :: XXREAL_2:86
for A being ext-real-membered set st ( for y, r being ext-real number st y in A &amp; inf A < r &amp; r < y holds
r in A ) holds
A is interval
proofend;

theorem :: XXREAL_2:87
for A being ext-real-membered set st ( for r being ext-real number st inf A < r &amp; r < sup A holds
r in A ) holds
A is interval
proofend;

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 &amp; y in A &amp; x <= r &amp; r <= y holds
r in A ) holds
A is interval
proofend;

theorem :: XXREAL_2:89
for A, B being ext-real-membered set st A is interval &amp; B is interval &amp; A meets B holds
A \/ B is interval
proofend;

theorem :: XXREAL_2:90
for A, B being ext-real-membered set st A is interval &amp; B is left_end &amp; B is interval &amp; sup A = inf B holds
A \/ B is interval
proofend;

theorem :: XXREAL_2:91
for A, B being ext-real-membered set st A is right_end &amp; A is interval &amp; B is interval &amp; sup A = inf B holds
A \/ B is interval
proofend;

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
proofend;
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
proofend;
end;

:: from HAHNBAN, 2011.04.26, A.T.
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}
proofend;

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}
proofend;

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 &amp; r < s )
proofend;

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 &amp; s < r )
proofend;

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 &amp; s in B holds
r <= s ) holds
sup A <= inf B
proofend;