:: AXIOMS semantic presentation

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

{ [b

1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT

{ [b

{ [b

bool { [b

( { [b

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+

{ b

x9 is set

y9 is Element of REAL+

[0,y9] is set

{0,y9} is set

{{0,y9},{0}} is set

{ b

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

{ b

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+