:: REAL semantic presentation

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