:: 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 & i <= F2() & P1[i] ) } is finite
proof 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 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 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 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 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 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 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 ;
attr X is left_end means :Def5: :: XXREAL_2:def 5
inf X in X;
attr X 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 end;

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

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

Lm2: for x being ext-real number holds inf {x} = x
proof 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 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 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 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 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 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 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 end;

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

theorem Th10: :: XXREAL_2:10
for A, B being ext-real-membered set holds sup (A \/ B) = max ((sup A),(sup B))
proof 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 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 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 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 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 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 end;

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

proof end;

theorem :: XXREAL_2:12
for x, y being ext-real number holds max (x,y) = max {x,y}
proof 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 end;

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

proof end;

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

definition
let X be ext-real-membered set ;
attr X is bounded_below means :Def9: :: XXREAL_2:def 9
ex r being real number st r is LowerBound of X;
attr X 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 end;
end;

definition
let X be ext-real-membered set ;
attr X 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 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 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 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 end;

registration
let X be real-membered non empty bounded_above set ;
cluster sup X -> ext-real real ;
coherence
sup X is real
proof 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 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 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 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 end;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th32: :: XXREAL_2:32
for x, y being ext-real number st x < y holds
sup ].x,y.[ = y
proof 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 end;

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

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

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

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

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

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

theorem Th40: :: XXREAL_2:40
for X being ext-real-membered set holds
( not X is empty iff inf X <= sup X )
proof 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 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 end;

theorem :: XXREAL_2:42
for X being ext-real-membered set holds -infty is LowerBound of X
proof 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 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 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 end;

theorem Th46: :: XXREAL_2:46
( not REAL is bounded_below & not REAL is bounded_above )
proof 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 end;

theorem :: XXREAL_2:48
{-infty} is bounded_above
proof 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 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 end;

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

theorem Th52: :: XXREAL_2:52
for X being ext-real-membered set st +infty is LowerBound of X holds
X c= {+infty}
proof 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 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 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 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 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 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 end;

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

theorem :: XXREAL_2:60
for X, Y being ext-real-membered set st X c= Y holds
inf Y <= inf X
proof 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 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 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 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 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 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 end;

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

theorem :: XXREAL_2:68
for X, Y being ext-real-membered set holds max ((inf X),(inf Y)) <= inf (X /\ Y)
proof 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 end;
end;

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

theorem :: XXREAL_2:70
for A being ext-real-membered set st sup A = inf A holds
A = {(inf A)}
proof 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 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 end;

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

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

begin

definition
let A be ext-real-membered set ;
attr A 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 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 end;
let r, s be ext-real number ;
cluster [.r,s.] -> interval ;
coherence
[.r,s.] is interval
proof end;
cluster ].r,s.] -> interval ;
coherence
].r,s.] is interval
proof end;
cluster [.r,s.[ -> interval ;
coherence
[.r,s.[ is interval
proof end;
cluster ].r,s.[ -> interval ;
coherence
].r,s.[ is interval
proof 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 end;
end;

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

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