:: XXREAL_1 semantic presentation

K6(REAL) is set

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

{ b1 where b1 is ext-real Element of ExtREAL : P1[b1] } is set
{ b1 where b1 is ext-real Element of ExtREAL : P2[b1] } is set
{ b1 where b1 is ext-real Element of ExtREAL : P1[b1] } /\ REAL is complex-membered ext-real-membered real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : P2[b1] } /\ REAL is complex-membered ext-real-membered real-membered set

p is ext-real set
p is ext-real set

p is ext-real set
p is ext-real set

p is ext-real set

p is ext-real set
p is ext-real set
p is ext-real set

t is ext-real set
r is ext-real set

r is ext-real set

r is ext-real set
s is ext-real set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set

r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set

r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set

r is ext-real set
s is ext-real set
t is ext-real set
(s,t) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set

r is ext-real set
s is ext-real set
(r,s) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is set

(r,s) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is set

(r,s) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is set

(r,s) is set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is set

r is set
s is ext-real set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
r is ext-real set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= r ) } is set
{r} is non empty ext-real-membered set
s is ext-real set

r is ext-real set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not r <= b1 ) } is set
s is ext-real set
t is ext-real set

r is ext-real set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= r ) } is set
s is ext-real set

r is ext-real set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not r <= b1 ) } is set
s is ext-real set

r is ext-real set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= r ) } is set
{r} is non empty ext-real-membered set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not r <= b1 ) } is set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= r ) } is set
(r,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not r <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not r <= b1 ) } is set
t is ext-real set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not r <= b1 ) } is set
(s,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not r <= b1 ) } is set
r is ext-real set
s is ext-real set
(s,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
s is ext-real set
r is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
s is ext-real set
r is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= x ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= x ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= x ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= x ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
x is ext-real set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= r ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not r <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not r <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not r <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not r <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } is set
r is ext-real set
s is ext-real set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( x <= b1 & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= s ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not s <= b1 ) } is set
x is ext-real set
(x,r) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= x & not r <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
{s} is non empty ext-real-membered set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( max (r,t) <= b1 & not min (s,x) <= b1 ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( max (r,t) <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= max (r,t) & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= max (r,t) & not min (s,x) <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= x ) } is set
(r,t) /\ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( min (r,t) <= b1 & not max (s,x) <= b1 ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( min (r,t) <= b1 & not max (s,x) <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= min (r,t) & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= min (r,t) & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not s <= b1 ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not x <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= x ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= t ) } is set
x is ext-real set
(s,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & not x <= b1 ) } is set
(r,t) \/ (s,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } is set
p is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= t ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= t & b1 <= x ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= x ) } is set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & not x <= b1 ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not x <= b1 ) } is set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= r & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(s,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
(r,s) \/ (s,t) is ext-real-membered set
x is ext-real set
(t,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( t <= b1 & b1 <= x ) } is set
((r,s) \/ (s,t)) \/ (t,x) is ext-real-membered set
(r,x) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= x ) } is set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= s ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not t <= b1 ) } is set
x is ext-real set
r is ext-real set
s is ext-real set
(r,s) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= 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
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not s <= b1 ) } is set
t is ext-real set
(r,t) is ext-real-membered set
{ b1 where b1 is ext-real Element of ExtREAL : ( r <= b1 & not t <= b1 ) } 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
{ b1 where b1 is ext-real Element of ExtREAL : ( s