:: XXREAL_2 semantic presentation

+infty is ext-real positive non negative non real non empty set
-infty is ext-real non positive negative non real non empty set

is set
is non empty finite set

is non empty finite V37() set

F1() is ext-real real integer V51() set
F2() is ext-real real integer V51() set
{ F3(b1) where b1 is ext-real real integer rational V51() Element of INT : ( F1() <= b1 & b1 <= F2() & P1[b1] ) } is set
B is set

F3(s1) is set

F2() - F1() is ext-real real integer V51() set

x is set

y + F1() is ext-real real integer V51() set
F3((y + F1())) is set

dom x is set
rng x is set
y is set

F3(r) is set
r - F1() is ext-real real integer V51() set

x . (r - F1()) is set
r + F1() is ext-real real integer V51() set
(r + F1()) - F1() is ext-real real integer V51() set
F3(((r + F1()) - F1())) is set

c8 + F1() is ext-real real integer V51() set
F3((c8 + F1())) is set

B is ext-real set
B is ext-real set

B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real (A)
B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real set
B is ext-real set
s1 is ext-real (A)
B is ext-real set
s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set

({A}) is ext-real set
B is ext-real ({A})
A is ext-real set

({A}) is ext-real set
B is ext-real ({A})

A is ext-real set

(B) is ext-real set
A is ext-real set

(B) is ext-real set

s1 is ext-real (B)
x is ext-real set

s1 is ext-real (B)
x is ext-real set

s1 is ext-real (A)
x is ext-real (B)
min (s1,x) is ext-real set
r is ext-real set

s1 is ext-real (A)
x is ext-real (B)
max (s1,x) is ext-real set
r is ext-real set

(A) is ext-real set

((A \/ B)) is ext-real set
(B) is ext-real set
min ((A),(B)) is ext-real set
x is ext-real (A \/ B)

(A) is ext-real set

((A \/ B)) is ext-real set
(B) is ext-real set
max ((A),(B)) is ext-real set
x is ext-real (A \/ B)

((B \/ s1)) is ext-real set
(B) is ext-real set
(s1) is ext-real set
min ((B),(s1)) is ext-real set
((B \/ s1)) is ext-real set
(B) is ext-real set
(s1) is ext-real set
max ((B),(s1)) is ext-real set

({B}) is ext-real set
({B}) is ext-real set

s1 is ext-real set
s1 is ext-real (A)
(A) is ext-real set
A is ext-real-membered () set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real (A)
A is ext-real-membered () set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real (A)
A is ext-real set
{A} is ext-real-membered non empty finite () () set
({A}) is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real ({A,B})
A is ext-real set
B is ext-real set
max (A,B) is ext-real set
{A,B} is ext-real-membered non empty finite () () set
({A,B}) is ext-real set
s1 is ext-real ({A,B})
s1 is ext-real ({A,B})
A is ext-real set
{A} is ext-real-membered non empty finite () () set
({A}) is ext-real set
A is ext-real set
B is ext-real set
{B,A} is ext-real-membered non empty finite () () set
s1 is ext-real set
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
s1 is ext-real ({A,B})
A is ext-real set
B is ext-real set
{A,B} is ext-real-membered non empty finite () () set
({A,B}) is ext-real set
min (A,B) is ext-real set
s1 is ext-real ({A,B})
s1 is ext-real ({A,B})

B is ext-real set
B is ext-real set

(B) is ext-real set
(A) is ext-real set
s1 is ext-real real V51() set
x is ext-real set
(B) is ext-real set
(A) is ext-real set
x is ext-real real V51() set
y is ext-real set

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() set

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() set

(A) is ext-real set

(A) is ext-real set

(B) is ext-real real V51() set

x is ext-real set
(A) is ext-real set

x - 1 is ext-real real integer V51() set
y is ext-real set

(B) is ext-real real V51() set

x is ext-real set
(A) is ext-real set

x + 1 is ext-real real integer V51() set
y is ext-real set

B is ext-real set

(A) is ext-real set

(A) is ext-real real V51() set

(A) is ext-real real rational V51() set

(A) is ext-real set

(A) is ext-real real V51() set

(A) is ext-real real rational V51() set

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real set

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

s1 is ext-real set
A is ext-real set
B is ext-real set

([.A,B.]) is ext-real set
s1 is ext-real ([.A,B.])
A is ext-real set
B is ext-real set

([.A,B.[) is ext-real set
s1 is ext-real ([.A,B.[)
A is ext-real set
B is ext-real set

(].A,B.]) is ext-real set
s1 is ext-real (].A,B.])
x is ext-real set
A is ext-real set
B is ext-real set

(].A,B.[) is ext-real set
s1 is ext-real (].A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set

([.A,B.]) is ext-real set
s1 is ext-real ([.A,B.])
A is ext-real set
B is ext-real set

(].A,B.]) is ext-real set
s1 is ext-real (].A,B.])
A is ext-real set
B is ext-real set

([.A,B.[) is ext-real set
s1 is ext-real ([.A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set

(].A,B.[) is ext-real set
s1 is ext-real (].A,B.[)
x is ext-real set
A is ext-real set
B is ext-real set

([.A,B.]) is ext-real set
([.A,B.]) is ext-real set
A is ext-real set
B is ext-real set

([.A,B.[) is ext-real set
A is ext-real set
B is ext-real set

(].A,B.]) is ext-real set
A is ext-real set
B is ext-real set
A is ext-real set
B is ext-real set
({}) is ext-real set
A is ext-real ( {} )
({}) is ext-real set
A is ext-real ( {} )

(A) is ext-real set
(A) is ext-real set
B is ext-real set

{ H1(b1) where b1 is ext-real real integer rational V51() Element of INT : ( (B) <= b1 & b1 <= (B) & S1[b1] ) } is set

B is ext-real set

B is ext-real set

s1 is ext-real real V51() set

s1 is ext-real real V51() set

A is ext-real real V51() set
B is ext-real real V51() set
A is ext-real real V51() set
B is ext-real real V51() set
is ext-real-membered non empty finite () () set
A is ext-real set
is ext-real-membered non empty finite () () set
A is ext-real set
A is ext-real-membered non empty () set
B is set
x is ext-real real V51() set
s1 is ext-real set
A is ext-real-membered non empty () set
B is set
x is ext-real real V51() set
s1 is ext-real set

B is ext-real set

B is ext-real set

B is ext-real (A)
s1 is ext-real set
s1 is ext-real real V51() set

B is ext-real (A)
s1 is ext-real set
s1 is ext-real real V51() set

(A) is ext-real set
B is ext-real (A)
s1 is ext-real (A)

(A) is ext-real set
B is ext-real (A)
s1 is ext-real (A)

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() Element of REAL

(A) is ext-real set
B is ext-real real V51() set
s1 is ext-real real V51() Element of REAL

(A) is ext-real set
(B) is ext-real set

(B) is ext-real set
(A) is ext-real set

(A) is ext-real set
B is ext-real set
s1 is ext-real set

(A) is ext-real set
B is ext-real set
s1 is ext-real set

(A) is ext-real set
(B) is ext-real set
s1 is ext-real set
x is ext-real set

(A) is ext-real set
(B) is ext-real set
s1 is ext-real set
x is ext-real set

s1 is ext-real (A)
x is ext-real (B)
min (s1,x) is ext-real set
y is ext-real set

s1 is ext-real (A)
x is ext-real (B)
max (s1,x) is ext-real set
y is ext-real set

((A /\ B)) is ext-real set
(A) is ext-real set
(B) is ext-real set
min ((A),(B)) is ext-real set

(A) is ext-real set

(B) is ext-real set
max ((A),(B)) is ext-real set

((A /\ B)) is ext-real set

B is set
s1 is ext-real-membered non empty set
x is ext-real real V51() set
y is ext-real set
r is ext-real real V51() set

(A) is ext-real set
(A) is ext-real set
[.(A),(A).] is ext-real-membered set
B is ext-real set

(A) is ext-real set
(A) is ext-real set
{(A)} is ext-real-membered non empty finite () () set
[.(A),(A).] is ext-real-membered non empty set
A is ext-real set
B is ext-real set

x is ext-real set
A is ext-real set
B is ext-real set

x is ext-real set

(A) is ext-real set
B is ext-real real V51() set

(A) is ext-real set
B is ext-real real V51() set
A is ext-real set
B is ext-real set

B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered set
A is ext-real set
B is ext-real set

s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered set
y is ext-real set

s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set

s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set

s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
y is ext-real set
A is ext-real-membered () set
B is ext-real-membered () set

s1 is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
A is ext-real set
B is ext-real set
].A,B.] is ext-real-membered () set
(].A,B.]) is ext-real set
[.A,B.[ is ext-real-membered () set
([.A,B.[) is ext-real set

(].A,B.[) is ext-real set
(].A,B.[) is ext-real set

A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
[.(A),(A).] is ext-real-membered () set
B is ext-real set
A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
].(A),(A).] is ext-real-membered () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
[.s1,(A).] is ext-real-membered () set
s1 is ext-real set
A is ext-real-membered () () () set
(A) is ext-real set
(A) is ext-real set
[.(A),(A).[ is ext-real-membered () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
[.(A),s1.] is ext-real-membered () set
s1 is ext-real set
A is ext-real-membered non empty () () () set
(A) is ext-real set
(A) is ext-real set
].(A),(A).[ is complex-membered ext-real-membered real-membered () () () set
B is ext-real set
s1 is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set
[.s1,x.] is ext-real-membered () set
s1 is ext-real set
x is ext-real set
A is ext-real-membered () () () set

(A) is ext-real set
(A) is ext-real set
].(A),(A).[ is complex-membered ext-real-membered real-membered () () () set

B is ext-real set
s1 is ext-real set
x is ext-real set
[.B,s1.] is ext-real-membered () set

(A) is ext-real set
B is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set

(A) is ext-real set
B is ext-real set
s1 is ext-real set
x is ext-real set
x is ext-real set

(A) is ext-real set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
s1 is ext-real set

B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set

(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set

(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set

(A) is ext-real set
(A) is ext-real set
B is ext-real set
s1 is ext-real set
[.B,s1.] is ext-real-membered () set
x is ext-real set
].B,s1.[ is complex-membered ext-real-membered real-membered () () () set
{B,s1} is ext-real-membered non empty finite () () set
].B,s1.[ \/ {B,s1} is ext-real-membered non empty set

B is ext-real set
s1 is ext-real set
x is ext-real set

s1 is ext-real set
x is ext-real set
y is ext-real set
r is ext-real set

(A) is ext-real set

(B) is ext-real set

x is ext-real set
y is ext-real set
r is ext-real set

(A) is ext-real set

(B) is ext-real set

x is ext-real set
y is ext-real set
r is ext-real set

(A) is ext-real set

(A) is ext-real set

A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real Element of A
A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real Element of A
A is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set
B is ext-real set
s1 is ext-real set
A is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set

s1 is ext-real set
A is ext-real-membered non empty Element of K12(ExtREAL)
B is ext-real-membered non empty Element of K12(ExtREAL)
(A) is ext-real set
(B) is ext-real set
s1 is ext-real Element of ExtREAL