REAL is V1() set
NAT is V1() epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is set
omega is V1() epsilon-transitive epsilon-connected ordinal set
RAT+ is set
bool RAT+ is set
bool (bool RAT+) is set
DEDEKIND_CUTS is Element of bool (bool RAT+)
REAL+ is set
K58() is Element of RAT+
the V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real set is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real set
{K58()} is set
[:{K58()},REAL+:] is set
one is V1() epsilon-transitive epsilon-connected ordinal Element of RAT+
0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real real Element of NAT
{0} is set
[:{0},REAL+:] is set
-infty is V1() ext-real non positive negative non real set
+infty is V1() ext-real positive non negative non real set
RP is V11() ext-real real Element of REAL
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real Element of NAT
RP is V11() ext-real real Element of REAL
- RP is V11() ext-real real set
RP " is V11() ext-real real set
RP is V11() ext-real real set
e is V11() ext-real real Element of REAL
RP + e is V11() ext-real real set
RP * e is V11() ext-real real set
RP - e is V11() ext-real real set
RP / e is V11() ext-real real set
RP is V11() ext-real real Element of REAL
e is V11() ext-real real set
RP + e is V11() ext-real real set
RP * e is V11() ext-real real set
RP - e is V11() ext-real real set
RP / e is V11() ext-real real set
{ b1 where b1 is V11() ext-real real Element of REAL : 0 <= b1 } is set
e is set
r is V11() ext-real real Element of REAL
o is Element of REAL+
s is Element of REAL+
e is set
r is V11() ext-real real Element of REAL