:: AXIOMS semantic presentation

REAL is non empty set

K99() is set
{} is set

{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set

{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of omega : verum } ) \/ omega is set
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
is set

is set

is set

is set
is set
is set
is set
() \ is Element of bool ()
bool () is set
-infty is non real set
is set
is set
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},} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},} 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},} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},} 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},} is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},} 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

y9 is V28() ext-real real set
x9 is V28() ext-real real set
o is Element of REAL+
x0 is Element of REAL+
{ b1 where b1 is Element of REAL+ : [0,b1] in k } is set
x9 is set
y9 is Element of REAL+
[0,y9] is set
{0,y9} is set
{{0,y9},} is set
{ b1 where b1 is Element of REAL+ : [0,b1] in e } is set
y9 is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} 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},} 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},} 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},} is set
[0,x9] is set
{0,x9} is set
{{0,x9},} is set
e is Element of REAL+
[0,e] is set
{0,e} is set
{{0,e},} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} 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},} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} is set
e is Element of REAL+
[0,e] is set
{0,e} is set
{{0,e},} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} is set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} 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},} 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},} is set

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

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+

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V28() ext-real real Element of NAT : not k <= b1 } is set
i is set

y9 is Element of REAL+
x9 is Element of REAL+

e is set

y9 is Element of REAL+
x9 is Element of REAL+