REAL is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
K99() is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() ext-real real set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() ext-real real set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } ) \/ omega is set
bool K99() is set
bool (bool K99()) is set
DEDEKIND_CUTS is non empty Element of bool (bool K99())
REAL+ is non empty set
COMPLEX is non empty set
K105() is Element of K99()
{K105()} is set
[:{K105()},REAL+:] is set
0 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
{0} is set
[:{0},REAL+:] is set
bool REAL+ is set
K106() is non empty epsilon-transitive epsilon-connected ordinal Element of K99()
{{}} is set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is set
[{},{}] is set
{{},{}} is set
{{{},{}},{{}}} is set
{[{},{}]} is set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is set
-infty is non real set
[0,REAL] is set
{0,REAL} is set
{{0,REAL},{0}} is set
+infty is non real set
o is V28() ext-real real set
k is V28() ext-real real set
e is Element of REAL+
i is Element of REAL+
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
e is Element of REAL+
i is Element of REAL+
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
e is Element of REAL+
i is Element of REAL+
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
o is V28() ext-real real set
k is V28() ext-real real Element of REAL
e is V28() ext-real real Element of REAL
[*k,e*] is Element of COMPLEX
(0,1) --> (k,e) is V6() V18({0,1}, REAL ) Element of bool [:{0,1},REAL:]
{0,1} is set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set
o is V28() ext-real real Element of REAL
k is V28() ext-real real Element of REAL
+ (o,k) is V28() ext-real real Element of REAL
e is V28() ext-real real set
i is V28() ext-real real set
e + i is V28() ext-real real set
x9 is V28() ext-real real Element of REAL
y9 is V28() ext-real real Element of REAL
[*x9,y9*] is Element of COMPLEX
x9 is V28() ext-real real Element of REAL
x0 is V28() ext-real real Element of REAL
[*x9,x0*] is Element of COMPLEX
+ (x9,x9) is V28() ext-real real Element of REAL
+ (y9,x0) is V28() ext-real real Element of REAL
[*(+ (x9,x9)),(+ (y9,x0))*] is Element of COMPLEX
k is Element of bool REAL
e is Element of bool REAL
i is V28() ext-real real set
x9 is V28() ext-real real set
i is V28() ext-real real Element of REAL
REAL+ \/ [:{0},REAL+:] is set
x9 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
y9 is V28() ext-real real set
x9 is V28() ext-real real set
o is Element of REAL+
x0 is Element of REAL+
{ b1 where b1 is Element of REAL+ : [0,b1] in k } is set
x9 is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
{ b1 where b1 is Element of REAL+ : [0,b1] in e } is set
y9 is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
x9 is set
x0 is set
Y9 is set
[x0,Y9] is set
{x0,Y9} is set
{x0} is set
{{x0,Y9},{x0}} is set
z9 is Element of REAL+
[0,z9] is set
{0,z9} is set
{{0,z9},{0}} is set
z is V28() ext-real real set
y9 is Element of bool REAL+
x is set
y is V28() ext-real real set
x is set
y is set
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
x9 is Element of bool REAL+
x9 is Element of REAL+
z is Element of REAL+
[0,z] is set
{0,z} is set
{{0,z},{0}} is set
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
e is Element of REAL+
[0,e] is set
{0,e} is set
{{0,e},{0}} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
x is V28() ext-real real set
y is V28() ext-real real set
e is Element of REAL+
[0,e] is set
{0,e} is set
{{0,e},{0}} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
e is Element of REAL+
[0,e] is set
{0,e} is set
{{0,e},{0}} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
z is V28() ext-real real set
x is V28() ext-real real set
y is V28() ext-real real set
e is set
x9 is set
[e,x9] is set
{e,x9} is set
{e} is set
{{e,x9},{e}} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},{0}} is set
e is set
y9 is set
[e,y9] is set
{e,y9} is set
{e} is set
{{e,y9},{e}} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},{0}} is set
k /\ REAL+ is Element of bool REAL
y9 is set
x9 is Element of REAL+
Y9 is set
z9 is V28() ext-real real set
x0 is V28() ext-real real set
x9 is Element of bool REAL+
Y9 is Element of bool REAL+
z9 is Element of REAL+
z is Element of REAL+
x is V28() ext-real real set
y is V28() ext-real real set
y9 is Element of REAL+
x9 is Element of REAL+
z9 is V28() ext-real real Element of REAL
z9 is Element of REAL+
z is V28() ext-real real set
x is V28() ext-real real set
y is V28() ext-real real set
x0 is V28() ext-real real set
x9 is Element of REAL+
y9 is Element of REAL+
y9 is Element of REAL+
k is V28() ext-real real set
e is V28() ext-real real set
k + e is V28() ext-real real set
i is V28() ext-real real Element of REAL
x9 is V28() ext-real real Element of REAL
+ (i,x9) is V28() ext-real real Element of REAL
y9 is Element of REAL+
x9 is Element of REAL+
y9 + x9 is Element of REAL+
k is Element of bool REAL
k /\ REAL+ is Element of bool REAL
e is Element of bool REAL+
i is Element of REAL+
x9 is Element of REAL+
i + x9 is Element of REAL+
y9 is V28() ext-real real Element of REAL
x9 is V28() ext-real real set
x9 + 1 is V28() ext-real real set
+ (y9,1) is V28() ext-real real Element of REAL
x0 is Element of REAL+
Y9 is Element of REAL+
x0 + Y9 is Element of REAL+
k is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT : not k <= b1 } is set
i is set
e is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
y9 is Element of REAL+
x9 is Element of REAL+
x9 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
e is set
i is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT
y9 is Element of REAL+
x9 is Element of REAL+