:: XXREAL_1 semantic presentation

REAL is non empty complex-membered ext-real-membered real-membered V21() set
K6(REAL) is set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Element of K6(REAL)
ExtREAL is non empty ext-real-membered set
+infty is non empty ext-real positive non negative non real set
-infty is non empty ext-real non positive negative non real set
{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() set
the empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() set is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() set
{ b₁ where b₁ is ext-real Element of ExtREAL : P₁[b₁] } is set
{ b₁ where b₁ is ext-real Element of ExtREAL : P₂[b₁] } is set
{ b₁ where b₁ is ext-real Element of ExtREAL : P₁[b₁] } /\ REAL is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : P₂[b₁] } /\ REAL is complex-membered ext-real-membered real-membered set
t is complex-membered ext-real-membered real-membered Element of K6(REAL)
p is ext-real set
p is ext-real set
t is ext-real Element of ExtREAL
p is ext-real set
p is ext-real set
x is complex-membered ext-real-membered real-membered Element of K6(REAL)
p is ext-real set
t is ext-real Element of ExtREAL
p is ext-real set
p is ext-real set
p is ext-real set
t is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex-membered ext-real-membered real-membered Element of K6(REAL)
p is ext-real real set
t is ext-real real set
r is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
p is ext-real real set
t is ext-real set
r is ext-real set
x is ext-real real Element of REAL
r is ext-real real set
r is ext-real Element of ExtREAL
r is ext-real set
x is ext-real real Element of REAL
r is ext-real real set
r is ext-real Element of ExtREAL
t is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex-membered ext-real-membered real-membered Element of K6(REAL)
r is ext-real set
s is ext-real set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real Element of ExtREAL
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real Element of ExtREAL
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real Element of ExtREAL
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real Element of ExtREAL
r is ext-real set
s is ext-real set
(r,s) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is set
x is ext-real Element of ExtREAL
(r,s) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is set
x is ext-real Element of ExtREAL
(r,s) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is set
x is ext-real Element of ExtREAL
(r,s) is set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is set
x is ext-real Element of ExtREAL
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
r is ext-real set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
{r} is non empty ext-real-membered set
s is ext-real set
t is ext-real Element of ExtREAL
t is ext-real Element of ExtREAL
r is ext-real set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not r <= b₁ ) } is set
s is ext-real set
t is ext-real set
x is ext-real Element of ExtREAL
r is ext-real set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= r ) } is set
s is ext-real set
t is ext-real Element of ExtREAL
r is ext-real set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not r <= b₁ ) } is set
s is ext-real set
t is ext-real Element of ExtREAL
r is ext-real set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
{r} is non empty ext-real-membered set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not r <= b₁ ) } is set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= r ) } is set
(r,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
s is ext-real set
r is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
s is ext-real set
r is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{r,s} is non empty ext-real-membered set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & not r <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & not r <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & not r <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & b₁ <= r ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & b₁ <= r ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & not r <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & not r <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & not r <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & not r <= b₁ ) } is set
p is ext-real set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{r,s} is non empty ext-real-membered set
(r,s) \/ {r,s} is non empty ext-real-membered set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
{s} is non empty ext-real-membered set
(r,s) \/ {s} is non empty ext-real-membered set
t is ext-real set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{r} \/ (r,s) is non empty ext-real-membered set
t is ext-real set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{r} \/ (r,s) is non empty ext-real-membered set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{s} is non empty ext-real-membered set
(r,s) \/ {s} is non empty ext-real-membered set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{r,s} is non empty ext-real-membered set
(r,s) \ {r,s} is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) \/ {r,s} is non empty ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) \ {r} is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{r} \/ (r,s) is non empty ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
(r,s) \ {s} is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) \/ {s} is non empty ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) \ {r} is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{r} \/ (r,s) is non empty ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
(r,s) \ {s} is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) \/ {s} is non empty ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) /\ (s,t) is ext-real-membered set
x is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
max (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(r,s) /\ (t,x) is ext-real-membered set
min (s,x) is ext-real set
((max (r,t)),(min (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( max (r,t) <= b₁ & not min (s,x) <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
max (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
(r,s) /\ (t,x) is ext-real-membered set
min (s,x) is ext-real set
((max (r,t)),(min (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( max (r,t) <= b₁ & b₁ <= min (s,x) ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
max (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(r,s) /\ (t,x) is ext-real-membered set
min (s,x) is ext-real set
((max (r,t)),(min (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= max (r,t) & b₁ <= min (s,x) ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
max (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
(r,s) /\ (t,x) is ext-real-membered set
min (s,x) is ext-real set
((max (r,t)),(min (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= max (r,t) & not min (s,x) <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
(r,t) /\ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
min (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(r,s) \/ (t,x) is ext-real-membered set
max (s,x) is ext-real set
((min (r,t)),(max (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( min (r,t) <= b₁ & not max (s,x) <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
min (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(r,s) \/ (t,x) is ext-real-membered set
max (s,x) is ext-real set
((min (r,t)),(max (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( min (r,t) <= b₁ & not max (s,x) <= b₁ ) } is set
p is ext-real set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
min (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(r,s) \/ (t,x) is ext-real-membered set
max (s,x) is ext-real set
((min (r,t)),(max (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= min (r,t) & b₁ <= max (s,x) ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
min (r,t) is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(r,s) \/ (t,x) is ext-real-membered set
max (s,x) is ext-real set
((min (r,t)),(max (s,x))) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= min (r,t) & b₁ <= max (s,x) ) } is set
p is ext-real set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ (t,x) is ext-real-membered set
(r,s) \/ {} is ext-real-membered set
((r,s) \/ {}) \/ (t,x) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \/ (t,x) is ext-real-membered set
(r,s) \/ {} is ext-real-membered set
((r,s) \/ {}) \/ (t,x) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ (t,x) is ext-real-membered set
(r,s) \/ {} is ext-real-membered set
((r,s) \/ {}) \/ (t,x) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(t,s) \ (r,s) is ext-real-membered Element of K6((t,s))
K6((t,s)) is set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not x <= b₁ ) } is set
(r,s) \ (t,x) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(x,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( x <= b₁ & not s <= b₁ ) } is set
(r,t) \/ (x,s) is ext-real-membered set
p is ext-real set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= x ) } is set
(r,s) \ (t,x) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(x,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= x & b₁ <= s ) } is set
(r,t) \/ (x,s) is ext-real-membered set
p is ext-real set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= x ) } is set
(r,s) \/ (t,x) is ext-real-membered set
(r,x) \ ((r,s) \/ (t,x)) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(r,x) \ (r,s) is ext-real-membered Element of K6((r,x))
((r,x) \ (r,s)) \ (t,x) is ext-real-membered Element of K6((r,x))
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(s,x) \ (t,x) is ext-real-membered Element of K6((s,x))
K6((s,x)) is set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,r) \/ (r,t) is ext-real-membered set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,r) \/ (r,t) is ext-real-membered set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,r) \/ (r,t) is ext-real-membered set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,r) \/ (r,t) is ext-real-membered set
(-infty,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= +infty ) } is set
r is ext-real set
r is ext-real set
(r,-infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not -infty <= b₁ ) } is set
s is set
t is ext-real set
r is ext-real set
(r,-infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not -infty <= b₁ ) } is set
s is set
t is ext-real set
r is ext-real set
(r,-infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= -infty ) } is set
s is set
t is ext-real set
r is ext-real set
(r,-infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= -infty ) } is set
s is set
t is ext-real set
r is ext-real set
(+infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= +infty & not r <= b₁ ) } is set
s is set
t is ext-real set
r is ext-real set
(+infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( +infty <= b₁ & not r <= b₁ ) } is set
s is set
t is ext-real set
r is ext-real set
(+infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= +infty & b₁ <= r ) } is set
s is set
t is ext-real set
r is ext-real set
(+infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( +infty <= b₁ & b₁ <= r ) } is set
s is set
t is ext-real set
r is ext-real set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
(r,s) \/ (s,r) is ext-real-membered set
{r} is non empty ext-real-membered set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
x is ext-real set
(t,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not x <= b₁ ) } is set
(s,t) \/ (t,x) is ext-real-membered set
(-infty,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not +infty <= b₁ ) } is set
r is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
s is ext-real set
r is ext-real real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
r is ext-real real set
s is ext-real real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
{ b₁ where b₁ is ext-real real Element of REAL : not r <= b₁ } is set
s is ext-real real set
s is set
t is ext-real real Element of REAL
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
{ b₁ where b₁ is ext-real real Element of REAL : not b₁ <= r } is set
s is ext-real real set
s is set
t is ext-real real Element of REAL
r is ext-real real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
{ b₁ where b₁ is ext-real real Element of REAL : b₁ <= r } is set
s is ext-real real set
s is set
t is ext-real real Element of REAL
r is ext-real real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
{ b₁ where b₁ is ext-real real Element of REAL : r <= b₁ } is set
s is ext-real real set
s is set
t is ext-real real Element of REAL
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
t is ext-real real set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
s is ext-real set
r is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
r is ext-real set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(-infty,s) /\ (r,+infty) is complex-membered ext-real-membered real-membered set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(-infty,s) /\ (r,+infty) is complex-membered ext-real-membered real-membered set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(-infty,r) /\ (s,+infty) is complex-membered ext-real-membered real-membered set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
r is ext-real real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(-infty,r) /\ (s,+infty) is complex-membered ext-real-membered real-membered set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
p is ext-real real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not r <= b₁ ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
p is ext-real set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(-infty,r) \ (-infty,s) is complex-membered ext-real-membered real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
(-infty,r) \ (-infty,s) is complex-membered ext-real-membered real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not r <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
s is ext-real real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(r,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
(r,x) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(r,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
(r,x) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(r,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
(r,x) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(r,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not x <= b₁ ) } is set
(r,x) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
(r,t) \/ (s,x) is complex-membered ext-real-membered real-membered set
p is ext-real real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not x <= b₁ ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not x <= b₁ ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= x ) } is set
(r,x) \ (t,s) is ext-real-membered Element of K6((r,x))
K6((r,x)) is set
(s,x) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
p is ext-real set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \ {s} is complex-membered ext-real-membered real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is complex-membered ext-real-membered real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
{s} is non empty ext-real-membered set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ {s} is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,s) \ (t,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \/ {s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,s) \ (t,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ {s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,s) \ (t,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \/ {s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,s) \ (t,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ {s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
{r} \/ (s,t) is non empty ext-real-membered set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
{r} \/ (s,t) is non empty ext-real-membered set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not t <= b₁ ) } is set
{r} \/ (s,t) is non empty ext-real-membered set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \ (r,s) is ext-real-membered Element of K6((r,t))
K6((r,t)) is set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= t ) } is set
{r} \/ (s,t) is non empty ext-real-membered set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
s is ext-real set
r is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
s is ext-real set
r is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is complex-membered ext-real-membered real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(-infty,s) \ (r,t) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(-infty,s) \ (r,t) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(-infty,r) \/ (t,s) is complex-membered ext-real-membered real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
t is ext-real real set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(-infty,s) \ (r,t) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(-infty,r) \/ (t,s) is ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
(-infty,s) \ {r} is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,r) \/ (r,s) is ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,s) \ {r} is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(-infty,r) \/ (r,s) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,s) \ (r,s) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
{s} is non empty ext-real-membered set
(-infty,r) \/ {s} is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(-infty,s) \ (r,s) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
{s} is non empty ext-real-membered set
(-infty,r) \/ {s} is non empty ext-real-membered set
{-infty} is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= r ) } is set
{-infty} \/ (s,r) is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
s is ext-real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(-infty,r) \ (-infty,s) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
{-infty} \/ (s,r) is non empty ext-real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
(-infty,s) \ (-infty,r) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
{-infty} \/ (r,s) is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not s <= b₁ ) } is set
(-infty,s) \ (-infty,r) is ext-real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
{-infty} \/ (r,s) is non empty ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
(-infty,s) \ {r} is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,r) \/ (r,s) is complex-membered ext-real-membered real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
{s} is non empty complex-membered ext-real-membered real-membered set
(-infty,r) \ {s} is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not s <= b₁ ) } is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
(-infty,s) \/ (s,r) is ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,s) \ (r,s) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
{s} is non empty complex-membered ext-real-membered real-membered set
(-infty,r) \/ {s} is non empty ext-real-membered set
r is ext-real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
s is ext-real real set
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(-infty,s) \ (r,s) is complex-membered ext-real-membered real-membered Element of K6((-infty,s))
K6((-infty,s)) is set
{s} is non empty complex-membered ext-real-membered real-membered set
(-infty,r) \/ {s} is non empty complex-membered ext-real-membered real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,+infty) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(r,t) \/ (s,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
t is ext-real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( t <= b₁ & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
{s} is non empty ext-real-membered set
(r,+infty) \ {s} is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(r,s) \/ (s,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
{s} is non empty ext-real-membered set
(r,+infty) \ {s} is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(r,s) \/ (s,+infty) is ext-real-membered set
s is ext-real set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
{s} is non empty ext-real-membered set
(r,+infty) \ {s} is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,s) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
{s} is non empty ext-real-membered set
(r,+infty) \ {s} is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(r,s) \/ (s,+infty) is ext-real-membered set
{+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) \/ {+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) \ (s,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) \/ {+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(s,+infty) \ (r,+infty) is ext-real-membered Element of K6((s,+infty))
K6((s,+infty)) is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
(s,r) \/ {+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(s,+infty) \ (r,+infty) is ext-real-membered Element of K6((s,+infty))
K6((s,+infty)) is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
(s,r) \/ {+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,+infty) \ (r,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
{r} \/ (s,+infty) is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(r,+infty) \ (r,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
{r} \/ (s,+infty) is non empty ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
(-infty,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not +infty <= b₁ ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
(-infty,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= +infty ) } is set
r is ext-real set
s is ext-real real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
REAL \ (r,s) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(-infty,r) \/ (s,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
s is ext-real real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real real set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
REAL \ (r,s) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
(-infty,r) \/ (s,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
s is ext-real real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(-infty,+infty) \ (r,s) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= +infty ) } is set
(-infty,r) \/ (s,+infty) is ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
(-infty,+infty) \ {r} is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(-infty,r) \/ (r,+infty) is ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
(-infty,+infty) \ {r} is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
(-infty,r) \/ (r,+infty) is ext-real-membered set
r is ext-real set
{r} is non empty ext-real-membered set
REAL \ {r} is complex-membered ext-real-membered real-membered Element of K6(REAL)
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(-infty,r) \/ (r,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real real set
{r} is non empty complex-membered ext-real-membered real-membered set
(-infty,+infty) \ {r} is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
(-infty,r) \/ (r,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
t is ext-real real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
t is ext-real real set
(t,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & not s <= b₁ ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
t is ext-real real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,+infty) \ (t,s) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not +infty <= b₁ ) } is set
t is ext-real real set
(t,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= t & b₁ <= s ) } is set
(r,+infty) \ (t,s) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= t ) } is set
(r,t) \/ (s,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
(s,+infty) \ (s,r) is complex-membered ext-real-membered real-membered Element of K6((s,+infty))
K6((s,+infty)) is set
{s} is non empty complex-membered ext-real-membered real-membered set
{s} \/ (r,+infty) is non empty complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
(-infty,+infty) \ (s,r) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,s) \/ (r,+infty) is ext-real-membered set
r is ext-real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
s is ext-real real set
(s,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
(-infty,+infty) \ (s,r) is ext-real-membered Element of K6((-infty,+infty))
K6((-infty,+infty)) is set
(-infty,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= s ) } is set
(-infty,s) \/ (r,+infty) is ext-real-membered set
s is ext-real real set
r is ext-real real set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
REAL \ (s,r) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
(-infty,s) \/ (r,+infty) is complex-membered ext-real-membered real-membered set
s is ext-real real set
r is ext-real real set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & b₁ <= r ) } is set
REAL \ (s,r) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(-infty,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= s ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(-infty,s) \/ (r,+infty) is complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
s is ext-real real set
(s,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not +infty <= b₁ ) } is set
(s,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= s & not r <= b₁ ) } is set
(s,+infty) \ (s,r) is complex-membered ext-real-membered real-membered Element of K6((s,+infty))
K6((s,+infty)) is set
{s} is non empty complex-membered ext-real-membered real-membered set
{s} \/ (r,+infty) is non empty ext-real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) \ (r,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
{s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) \ (r,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
{s} is non empty ext-real-membered set
(s,s) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= s ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
(r,s) \ (r,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
r is ext-real set
{r} is non empty ext-real-membered set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not s <= b₁ ) } is set
(r,s) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not s <= b₁ ) } is set
(r,s) \ (r,s) is ext-real-membered Element of K6((r,s))
K6((r,s)) is set
(r,r) is non empty ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= r ) } is set
r is ext-real real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(-infty,r) \ (-infty,r) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
{r} is non empty complex-membered ext-real-membered real-membered set
r is ext-real real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(-infty,r) \ (-infty,r) is complex-membered ext-real-membered real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
{r} is non empty complex-membered ext-real-membered real-membered set
r is ext-real real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
(-infty,r) \ (-infty,r) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
r is ext-real real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
(-infty,r) \ (-infty,r) is ext-real-membered Element of K6((-infty,r))
K6((-infty,r)) is set
r is ext-real real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) \ (r,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
r is ext-real real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(r,+infty) \ (r,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
r is ext-real real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
(r,+infty) \ (r,+infty) is ext-real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
{r} is non empty complex-membered ext-real-membered real-membered set
r is ext-real real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(r,+infty) \ (r,+infty) is complex-membered ext-real-membered real-membered Element of K6((r,+infty))
K6((r,+infty)) is set
{r} is non empty complex-membered ext-real-membered real-membered set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= t ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not t <= b₁ ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & not t <= b₁ ) } is set
(r,s) /\ (s,t) is ext-real-membered set
x is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) /\ (s,t) is ext-real-membered set
x is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(s,t) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( s <= b₁ & b₁ <= t ) } is set
(r,s) /\ (s,t) is ext-real-membered set
x is set
p is ext-real set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
{-infty,r} is non empty ext-real-membered set
(-infty,r) \/ {-infty,r} is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
{r} is non empty ext-real-membered set
(-infty,r) \/ {r} is non empty ext-real-membered set
r is ext-real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & b₁ <= r ) } is set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
{-infty} \/ (-infty,r) is non empty ext-real-membered set
r is ext-real real set
(-infty,r) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( -infty <= b₁ & not r <= b₁ ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
{-infty} \/ (-infty,r) is non empty ext-real-membered set
r is ext-real real set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & b₁ <= r ) } is set
(-infty,r) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= -infty & not r <= b₁ ) } is set
{r} is non empty complex-membered ext-real-membered real-membered set
(-infty,r) \/ {r} is non empty complex-membered ext-real-membered real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
{r,+infty} is non empty ext-real-membered set
(r,+infty) \/ {r,+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
(r,+infty) \/ {+infty} is non empty ext-real-membered set
r is ext-real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & b₁ <= +infty ) } is set
{r} is non empty ext-real-membered set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
{r} \/ (r,+infty) is non empty ext-real-membered set
r is ext-real real set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( r <= b₁ & not +infty <= b₁ ) } is set
{r} is non empty complex-membered ext-real-membered real-membered set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
{r} \/ (r,+infty) is non empty complex-membered ext-real-membered real-membered set
r is ext-real real set
(r,+infty) is ext-real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & b₁ <= +infty ) } is set
(r,+infty) is complex-membered ext-real-membered real-membered set
{ b₁ where b₁ is ext-real Element of ExtREAL : ( not b₁ <= r & not +infty <= b₁ ) } is set
(r,+infty) \/ {+infty} is non empty ext-real-membered set