:: XXREAL_0 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set

K32() is set

bool K32() is set

bool (bool K32()) is set

DEDEKIND_CUTS is Element of bool (bool K32())

REAL+ is set

REAL is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

{{}} is non empty set

[:{{}},REAL+:] is set

REAL+ \/ [:{{}},REAL+:] is set

[{},{}] is set

{{},{}} is non empty set

{{{},{}},{{}}} is non empty set

{[{},{}]} is non empty set

(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])

bool (REAL+ \/ [:{{}},REAL+:]) is set

bool REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

K38() is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of K32()

{K38()} is non empty set

[:{K38()},REAL+:] is set

ExtREAL is non empty set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of NAT

[0,REAL] is set

{0,REAL} is non empty set

{0} is non empty set

{{0,REAL},{0}} is non empty set

{REAL,[0,REAL]} is non empty set

REAL \/ {REAL,[0,REAL]} is non empty set

a is Element of ExtREAL

a is () set

() is set

() is set

{(),()} is non empty set

REAL \/ {(),()} is non empty set

a is set

b is set

a is () set

b is () set

[:{0},REAL+:] is set

a is Element of REAL+

b is Element of REAL+

c9 is Element of REAL+

[0,c9] is set

{0,c9} is non empty set

{{0,c9},{0}} is non empty set

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

a is () set

REAL+ \/ [:{0},REAL+:] is set

[0,0] is set

{0,0} is non empty set

{{0,0},{0}} is non empty set

{[0,0]} is non empty set

(REAL+ \/ [:{0},REAL+:]) \ {[0,0]} is Element of bool (REAL+ \/ [:{0},REAL+:])

bool (REAL+ \/ [:{0},REAL+:]) is set

b is Element of REAL+

b is set

c9 is set

[b,c9] is set

{b,c9} is non empty set

{b} is non empty set

{{b,c9},{b}} is non empty set

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

b is Element of REAL+

c9 is Element of REAL+

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

b9 is Element of REAL+

[0,b9] is set

{0,b9} is non empty set

{{0,b9},{0}} is non empty set

a is () set

b is () set

REAL+ \/ [:{0},REAL+:] is set

[0,0] is set

{0,0} is non empty set

{{0,0},{0}} is non empty set

{[0,0]} is non empty set

(REAL+ \/ [:{0},REAL+:]) \ {[0,0]} is Element of bool (REAL+ \/ [:{0},REAL+:])

bool (REAL+ \/ [:{0},REAL+:]) is set

a9 is Element of REAL+

c9 is Element of REAL+

b9 is Element of REAL+

x9 is Element of REAL+

c9 is set

a9 is set

[c9,a9] is set

{c9,a9} is non empty set

{c9} is non empty set

{{c9,a9},{c9}} is non empty set

b9 is set

x9 is set

[b9,x9] is set

{b9,x9} is non empty set

{b9} is non empty set

{{b9,x9},{b9}} is non empty set

y9 is Element of REAL+

x9 is Element of REAL+

y9 is Element of REAL+

[0,y9] is set

{0,y9} is non empty set

{{0,y9},{0}} is non empty set

x9 is Element of REAL+

[0,x9] is set

{0,x9} is non empty set

{{0,x9},{0}} is non empty set

c9 is Element of REAL+

[0,c9] is set

{0,c9} is non empty set

{{0,c9},{0}} is non empty set

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

c9 is Element of REAL+

a9 is Element of REAL+

b9 is Element of REAL+

[0,b9] is set

{0,b9} is non empty set

{{0,b9},{0}} is non empty set

x9 is Element of REAL+

[0,x9] is set

{0,x9} is non empty set

{{0,x9},{0}} is non empty set

[0,0] is set

{0,0} is non empty set

{{0,0},{0}} is non empty set

{{0},{0}} is non empty set

{{0}} is non empty set

REAL+ \/ [:{0},REAL+:] is set

a is () set

b is () set

a is Element of REAL+

b is Element of REAL+

c9 is Element of REAL+

a9 is Element of REAL+

a is Element of REAL+

[0,a] is set

{0,a} is non empty set

{{0,a},{0}} is non empty set

b is Element of REAL+

[0,b] is set

{0,b} is non empty set

{{0,b},{0}} is non empty set

c9 is Element of REAL+

[0,c9] is set

{0,c9} is non empty set

{{0,c9},{0}} is non empty set

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

a is () set

a is () set

a is () set

b is () set

a is () set

b is Element of REAL+

c9 is Element of REAL+

a9 is Element of REAL+

b9 is Element of REAL+

b is Element of REAL+

[0,b] is set

{0,b} is non empty set

{{0,b},{0}} is non empty set

c9 is Element of REAL+

[0,c9] is set

{0,c9} is non empty set

{{0,c9},{0}} is non empty set

a9 is Element of REAL+

[0,a9] is set

{0,a9} is non empty set

{{0,a9},{0}} is non empty set

b9 is Element of REAL+

[0,b9] is set

{0,b9} is non empty set

{{0,b9},{0}} is non empty set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

b is () set

a is () set

a is () set

b is () set

a is () set

a is set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

a is () set

b is () set

b is () set

c9 is () set

a is set

a is () set

b is () set

c9 is () set

b is () set

a is set

a is () set

b is () set

a is () set

b is () set

(a,b) is set

a is () set

b is () set

(a,b) is set

a is () set

b is () set

(a,b) is set

(a,b) is set

a is () set

b is () set

(a,b) is () set

a is () set

b is () set

a is () set

(a,a) is () set

b is () set

(b,b) is () set

a is () set

b is () set

a is () set

(a,a) is () set

b is () set

(b,b) is () set

a is () set

b is () set

a is () set

(b,a) is () set

b is () set

a is () set

a is () set

(b,a) is () set

a is () set

b is () set

a is () set

(b,a) is () set

a is () set

b is () set

a is () set

(b,a) is () set

a is () set

b is () set

a is () set

(b,a) is () set

a is () set

b is () set

(a,b) is () set

a is () set

b is () set

a is () set

(a,a) is () set

b is () set

(b,b) is () set

a is () set

b is () set

a is () set

(a,a) is () set

b is () set

(b,b) is () set

a is () set

b is () set

a is () set

(a,a) is () set

b is () set

a is () set

a is () set

(a,a) is () set

a is () set

b is () set

(a,b) is () set

a is () set

a is () set

b is () set

(a,b) is () set

a is () set

a is () set

b is () set

a is () set

(a,a) is () set

a is () set

b is () set

(a,b) is () set

a is () set

((a,b),a) is () set

(b,a) is () set

(a,(b,a)) is () set

(a,a) is () set

(a,a) is () set

a is () set

b is () set

(a,b) is () set

a is () set

((a,b),a) is () set

(b,a) is () set

(a,(b,a)) is () set

a is () set

b is () set

(a,b) is () set

((a,b),b) is () set

a is () set

b is () set

(a,b) is () set

((a,b),b) is () set

a is () set

b is () set

a is () set

(a,b) is () set

(a,(a,b)) is () set

(a,a) is () set

((a,a),b) is () set

(a,b) is () set

a is () set

b is () set

(a,b) is () set

a is () set

(b,a) is () set

(a,(b,a)) is () set

(a,a) is () set

((a,b),(a,a)) is () set

a is () set

b is () set

(a,b) is () set

a is () set

(b,a) is () set

(a,(b,a)) is () set

(a,a) is () set

((a,b),(a,a)) is () set

a is () set

b is () set

(a,b) is () set

(a,b) is () set

a is () set

(b,a) is () set

((a,b),(b,a)) is () set

(a,a) is () set

(((a,b),(b,a)),(a,a)) is () set

(b,a) is () set

((a,b),(b,a)) is () set

(a,a) is () set

(((a,b),(b,a)),(a,a)) is () set

((b,a),(a,a)) is () set

((b,a),a) is () set

((a,b),a) is () set

((a,b),(a,a)) is () set

((a,b),(a,a)) is () set

((a,b),a) is () set

(a,b) is () set

((a,b),a) is () set

((a,b),(a,a)) is () set

a is () set

(a,()) is () set

a is () set

(a,()) is () set

a is () set

(a,()) is () set

a is () set

(a,()) is () set

a is () set

b is () set

a is () set

a is () set

b is () set

a is () set

a is () set

b is () set

a is () set

a is () set

b is () set

a is () set

a is () set

b is () set

a is set

b is set

a is () set

b is () set

a is epsilon-transitive epsilon-connected ordinal natural () set

b is epsilon-transitive epsilon-connected ordinal natural () set

(a,b,a,b) is set

a is () set

b is () set

(a,b) is () set

a is () set

b is () set

(a,b) is () set