omega is non zero epsilon-transitive epsilon-connected ordinal set
K32() is set
bool K32() is set
bool (bool K32()) is set
DEDEKIND_CUTS is non zero Element of bool (bool K32())
REAL+ is non zero set
REAL is set
bool REAL is set
NAT is non zero epsilon-transitive epsilon-connected ordinal Element of bool REAL
K38() is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real real Element of K32()
{K38()} is non zero set
[:{K38()},REAL+:] is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real real set
{0} is non zero set
[:{0},REAL+:] is set
K2(REAL+,[:{0},REAL+:]) is non zero set
[0,0] is set
{[0,0]} is non zero set
K15(K2(REAL+,[:{0},REAL+:]),{[0,0]}) is Element of bool K2(REAL+,[:{0},REAL+:])
bool K2(REAL+,[:{0},REAL+:]) is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real real Element of NAT
{0} is non zero set
[:{0},REAL+:] is set
-infty is non real set
+infty is non real set
x is ext-real real set
y is ext-real real set
z is Element of REAL+
y99 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
z is Element of REAL+
[0,z] is set
y99 is Element of REAL+
[0,y99] is set
z9 is Element of REAL+
[0,z9] is set
x9 is Element of REAL+
[0,x9] is set
x is ext-real real set
y is ext-real real set
z is ext-real real set
y99 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
y9 is Element of REAL+
y99 is Element of REAL+
[0,y99] is set
z9 is Element of REAL+
[0,z9] is set
x9 is Element of REAL+
[0,x9] is set
y9 is Element of REAL+
[0,y9] is set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set
x is ext-real real set
y is ext-real real set