:: XXREAL_2 semantic presentation

REAL is complex-membered ext-real-membered real-membered V10() non empty V13() non finite set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() V13() non finite Element of K12(REAL)

K12(REAL) is V13() non finite cup-closed diff-closed preBoolean set

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

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

0 is ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() real empty ordinal natural integer finite V37() rational V51() Element of NAT

[0,REAL] is set

{0,REAL} is non empty finite set

{0} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V37() set

{{0,REAL},{0}} is non empty finite V37() set

ExtREAL is ext-real-membered non empty set

{+infty,-infty} is ext-real-membered non empty finite set

REAL \/ {+infty,-infty} is ext-real-membered non empty set

{} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() set

].-infty,+infty.[ is complex-membered ext-real-membered real-membered set

1 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() Element of NAT

INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V10() non empty V13() non finite set

F

F

{ F

B is set

s1 is ext-real real integer rational V51() Element of INT

F

B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() set

F

B is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real ordinal natural integer finite rational V51() Element of NAT

B + 1 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() Element of NAT

x is set

y is ext-real non negative real ordinal natural integer finite V51() set

y + F

F

x is Relation-like Function-like set

dom x is set

rng x is set

y is set

r is ext-real real integer rational V51() Element of INT

F

r - F

l is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real ordinal natural integer finite rational V51() Element of NAT

x . (r - F

r + F

(r + F

F

c

c

F

A is ext-real-membered set

B is ext-real set

B is ext-real set

A is ext-real-membered 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

{B} is ext-real-membered non empty finite set

s1 is ext-real set

A is ext-real set

B is ext-real set

{B} is ext-real-membered non empty finite set

s1 is ext-real set

A is ext-real set

{A} is ext-real-membered non empty finite set

({A}) is ext-real set

B is ext-real ({A})

A is ext-real set

{A} is ext-real-membered non empty finite set

({A}) is ext-real set

B is ext-real ({A})

Fin ExtREAL is non empty cup-closed diff-closed preBoolean set

A is finite Element of Fin ExtREAL

A is ext-real set

B is ext-real-membered set

(B) is ext-real set

A is ext-real set

B is ext-real-membered set

(B) is ext-real set

A is ext-real-membered set

B is ext-real-membered set

s1 is ext-real (B)

x is ext-real set

A is ext-real-membered set

B is ext-real-membered set

s1 is ext-real (B)

x is ext-real set

A is ext-real-membered set

B is ext-real-membered set

A \/ B is ext-real-membered set

s1 is ext-real (A)

x is ext-real (B)

min (s1,x) is ext-real set

r is ext-real set

A is ext-real-membered set

B is ext-real-membered set

A \/ B is ext-real-membered 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-membered set

(A) is ext-real set

B is ext-real-membered set

A \/ B is ext-real-membered 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-membered set

(A) is ext-real set

B is ext-real-membered set

A \/ B is ext-real-membered 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)

A is ext-real-membered non empty set

B is ext-real-membered non empty finite Element of Fin ExtREAL

s1 is ext-real-membered non empty finite Element of Fin ExtREAL

B \/ s1 is ext-real-membered non empty finite Element of Fin ExtREAL

((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 Element of ExtREAL

{.B.} is ext-real-membered non empty finite Element of Fin ExtREAL

{B} is ext-real-membered non empty finite set

({B}) is ext-real set

({B}) is ext-real set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty set

B is ext-real non negative real ordinal natural integer finite V51() 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})

A is ext-real-membered set

A is ext-real-membered set

A is complex-membered ext-real-membered real-membered set

B is ext-real set

B is ext-real set

B is complex-membered ext-real-membered real-membered non empty finite () () 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 complex-membered ext-real-membered real-membered non empty set

(A) is ext-real set

B is ext-real real V51() set

s1 is ext-real real V51() set

A is complex-membered ext-real-membered real-membered non empty set

(A) is ext-real set

B is ext-real real V51() set

s1 is ext-real real V51() set

A is complex-membered ext-real-membered real-membered non empty () set

(A) is ext-real set

A is complex-membered ext-real-membered real-membered non empty () set

(A) is ext-real set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty set

B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () set

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

[\(B)/] is ext-real real integer V51() set

x is ext-real set

(A) is ext-real set

x is ext-real real integer V51() set

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

y is ext-real set

r is ext-real real integer V51() set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty set

B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () set

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

[/(B)\] is ext-real real integer V51() set

x is ext-real set

(A) is ext-real set

x is ext-real real integer V51() set

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

y is ext-real set

r is ext-real real integer V51() set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

B is ext-real set

A is complex-membered ext-real-membered real-membered () set

(A) is ext-real set

A is complex-membered ext-real-membered real-membered rational-membered () set

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

A is complex-membered ext-real-membered real-membered rational-membered integer-membered () set

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

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered () () set

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

A is complex-membered ext-real-membered real-membered () set

(A) is ext-real set

A is complex-membered ext-real-membered real-membered rational-membered () set

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

A is complex-membered ext-real-membered real-membered rational-membered integer-membered () set

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

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered () () set

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

A is complex-membered ext-real-membered real-membered set

(A) is ext-real set

B is ext-real real V51() set

s1 is ext-real set

A is complex-membered ext-real-membered real-membered 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

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

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

s1 is ext-real set

A is ext-real set

B is ext-real set

[.A,B.] is ext-real-membered 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-membered 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-membered 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 complex-membered ext-real-membered real-membered 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-membered 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-membered 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-membered 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 complex-membered ext-real-membered real-membered 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-membered 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-membered set

([.A,B.[) is ext-real 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 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-membered set

(A) is ext-real set

(A) is ext-real set

B is ext-real set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered set

B is complex-membered ext-real-membered real-membered rational-membered integer-membered non empty () () () () () set

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

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

{ H

r is ext-real real integer V51() set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite () () () set

A is ext-real-membered set

B is ext-real set

A is ext-real-membered set

B is ext-real set

A is ext-real-membered set

B is ext-real-membered set

s1 is ext-real real V51() set

A is ext-real-membered set

B is ext-real-membered set

s1 is ext-real real V51() set

A is ext-real-membered set

B is ext-real-membered 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

{+infty} is ext-real-membered non empty finite () () set

A is ext-real set

{-infty} 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

A is ext-real-membered set

B is ext-real set

A is ext-real-membered set

B is ext-real set

A is ext-real-membered non empty set

B is ext-real (A)

s1 is ext-real set

s1 is ext-real real V51() set

A is ext-real-membered non empty set

B is ext-real (A)

s1 is ext-real set

s1 is ext-real real V51() set

A is ext-real-membered non empty set

(A) is ext-real set

B is ext-real (A)

s1 is ext-real (A)

A is ext-real-membered non empty set

(A) is ext-real set

B is ext-real (A)

s1 is ext-real (A)

A is ext-real-membered non empty set

(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-membered non empty set

(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-membered set

B is ext-real-membered set

(A) is ext-real set

(B) is ext-real set

A is ext-real-membered set

B is ext-real-membered set

(B) is ext-real set

(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

A is ext-real-membered set

(A) is ext-real set

B is ext-real set

s1 is ext-real set

A is ext-real-membered set

B 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

B is ext-real-membered set

A 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

A is ext-real-membered set

B is ext-real-membered set

A /\ B is ext-real-membered set

s1 is ext-real (A)

x is ext-real (B)

min (s1,x) is ext-real set

y is ext-real set

A is ext-real-membered set

B is ext-real-membered set

A /\ B is ext-real-membered set

s1 is ext-real (A)

x is ext-real (B)

max (s1,x) is ext-real set

y is ext-real set

A is ext-real-membered set

B is ext-real-membered set

A /\ B is ext-real-membered 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-membered set

(A) is ext-real set

B is ext-real-membered set

(B) is ext-real set

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

A /\ B is ext-real-membered set

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

A is ext-real-membered 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-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)} 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

s1 is ext-real-membered set

x is ext-real set

A is ext-real set

B is ext-real set

s1 is ext-real-membered set

x is ext-real set

A is ext-real-membered set

(A) is ext-real set

B is ext-real real V51() set

A is ext-real-membered set

(A) is ext-real set

B is ext-real real V51() set

A is ext-real set

B is ext-real set

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

A is ext-real-membered 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

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

s1 is ext-real set

x is ext-real set

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

y is ext-real set

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

s1 is ext-real set

x is ext-real set

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

y is ext-real set

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

s1 is ext-real set

x is ext-real set

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

y is ext-real set

].A,B.[ is complex-membered ext-real-membered real-membered 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

A /\ 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 complex-membered ext-real-membered real-membered () set

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

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

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

].0,1.] is complex-membered ext-real-membered real-membered () () set

[.0,1.[ is complex-membered ext-real-membered real-membered () () set

2 is ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered real non empty ordinal natural integer finite rational V51() () () () () () Element of NAT

].0,2.[ is complex-membered ext-real-membered real-membered () () () 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

].-infty,-infty.[ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V10() empty finite V37() () () () () () () set

(A) is ext-real set

(A) is ext-real set

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

A is ext-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-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-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-membered 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

A is ext-real-membered 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-membered 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-membered 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-membered 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

A is ext-real-membered set

B is ext-real set

s1 is ext-real set

x is ext-real set

A is ext-real-membered set

B is ext-real-membered set

A \/ B is ext-real-membered 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-membered set

(A) is ext-real set

B is ext-real-membered set

(B) is ext-real set

A \/ B is ext-real-membered set

x is ext-real set

y is ext-real set

r is ext-real set

A is ext-real-membered set

(A) is ext-real set

B is ext-real-membered set

(B) is ext-real set

A \/ B is ext-real-membered set

x is ext-real set

y is ext-real set

r is ext-real set

A is ext-real-membered set

(A) is ext-real set

A is ext-real-membered set

(A) is ext-real set

K12(ExtREAL) is cup-closed diff-closed preBoolean 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

B is ext-real Element of ExtREAL

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

x is ext-real Element of ExtREAL