:: REAL_1 semantic presentation

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

{ b

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