:: ARYTM_0 semantic presentation

REAL is non empty set

RAT+ is set

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

{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } ) \/ omega is non empty set

bool () is set
DEDEKIND_CUTS is non empty Element of bool ()
REAL+ is non empty set

{ b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
is set

is non empty trivial set
{ b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
\ is Element of bool { b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}

bool { b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
is set

RAT+ \/ DEDEKIND_CUTS is non empty set
{ { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is set
\ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is Element of bool

is non empty trivial set

REAL+ \/ is non empty set
is non empty set

() \ is Element of bool ()
bool () is set
COMPLEX is non empty set
{{},1} is non empty set
Funcs ({{},1},REAL) is functional non empty FUNCTION_DOMAIN of {{},1}, REAL
{ b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b1 . 1 = {} } is set
(Funcs ({{},1},REAL)) \ { b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b1 . 1 = {} } is functional Element of bool (Funcs ({{},1},REAL))
bool (Funcs ({{},1},REAL)) is set
((Funcs ({{},1},REAL)) \ { b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b1 . 1 = {} } ) \/ REAL is non empty set
is non empty trivial set

REAL+ \/ is non empty set
RR is Element of REAL+
[{},RR] is non empty set
is non empty set

REAL+ \/ is non empty set
RR is set
[{},RR] is non empty set
is non empty set

RR is Element of REAL+
o is Element of REAL+
RR - o is set
RR -' o is Element of REAL+
o -' RR is Element of REAL+
[{},(o -' RR)] is non empty set

RR is set
o is set
j is set
[o,j] is non empty set
RR is Element of REAL+
o is Element of REAL+
RR - o is set
o -' RR is Element of REAL+
[{},(o -' RR)] is non empty set
RR -' o is Element of REAL+
RR is set
o is set
[RR,o] is non empty set
{RR,o} is non empty set
{RR} is non empty trivial set
{{RR,o},{RR}} is non empty set
RR is Element of REAL+
o is Element of REAL+
RR *' o is Element of REAL+
j is Element of REAL+
RR *' j is Element of REAL+
o -' j is Element of REAL+
RR *' (o -' j) is Element of REAL+
(RR *' o) - (RR *' j) is set
o - j is set
j -' o is Element of REAL+
RR *' (j -' o) is Element of REAL+
(RR *' j) - (RR *' o) is set
j - o is set
RR is Element of REAL
o is Element of REAL

is non empty trivial set

j is Element of REAL+
x is Element of REAL+
j + x is Element of REAL+
y is Element of REAL
y9 is Element of REAL+
z9 is Element of REAL+
z is Element of REAL
y9 + z9 is Element of REAL+
REAL+ \/ is non empty set
x is set
y is set
[x,y] is non empty set
j is Element of REAL+
z is Element of REAL+
j - z is set
y9 is Element of REAL
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
z9 is Element of REAL
x9 - yz9 is set
x is set
y is set
[x,y] is non empty set
j is Element of REAL+
z is Element of REAL+
j - z is set
y9 is Element of REAL
x9 is Element of REAL+
[0,x9] is non empty set
yz9 is Element of REAL+
z9 is Element of REAL
yz9 - x9 is set
j is set
x is set
[j,x] is non empty set
y is set
z is set
[y,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
y9 + z9 is Element of REAL+
z9 + y9 is Element of REAL+
[0,(z9 + y9)] is non empty set
x9 is Element of REAL
[0,z9] is non empty set
[0,(y9 + z9)] is non empty set
j is Element of REAL
x is Element of REAL
y is Element of REAL+
z is Element of REAL+
y + z is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
y is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y - z is set
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 - z9 is set
y is Element of REAL+
[0,y] is non empty set
z is Element of REAL+
z - y is set
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
z9 - y9 is set
y is Element of REAL+
[0,y] is non empty set
z is Element of REAL+
[0,z] is non empty set
y + z is Element of REAL+
[0,(y + z)] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
y9 + z9 is Element of REAL+
[0,(y9 + z9)] is non empty set
x is Element of REAL+
y is Element of REAL+
j is Element of REAL
x + y is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z - y9 is set
x9 is Element of REAL+
yz9 is Element of REAL+
z9 is Element of REAL
x9 + yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
y99 - x99 is set
z99 is Element of REAL+
zy9 is Element of REAL+
[0,zy9] is non empty set
xy99 is Element of REAL
z99 - zy9 is set
c16 is Element of REAL+
[0,c16] is non empty set
c17 is Element of REAL+
c17 - c16 is set
x is Element of REAL
y is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
j is Element of REAL
z + y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 - x9 is set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 - yz9 is set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 + xy99 is Element of REAL+
[0,(y99 + xy99)] is non empty set
j is Element of REAL+
x is Element of REAL+
j *' x is Element of REAL+
y is Element of REAL
y9 is Element of REAL+
z9 is Element of REAL+
z is Element of REAL
y9 *' z9 is Element of REAL+
x is set
y is set
[x,y] is non empty set
z is Element of REAL+
[0,z] is non empty set
j is Element of REAL+
j *' z is Element of REAL+
[0,(j *' z)] is non empty set
y9 is Element of REAL
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
z9 is Element of REAL
x9 *' yz9 is Element of REAL+
[0,(x9 *' yz9)] is non empty set
x is set
y is set
[x,y] is non empty set
z is Element of REAL+
[0,z] is non empty set
j is Element of REAL+
j *' z is Element of REAL+
[0,(j *' z)] is non empty set
y9 is Element of REAL
x9 is Element of REAL+
[0,x9] is non empty set
yz9 is Element of REAL+
z9 is Element of REAL
yz9 *' x9 is Element of REAL+
[0,(yz9 *' x9)] is non empty set
j is set
x is set
[j,x] is non empty set
z is set
y9 is set
[z,y9] is non empty set
y is Element of REAL+
z9 is Element of REAL+
y *' z9 is Element of REAL+
z9 *' y is Element of REAL+
x9 is Element of REAL
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
yz9 is Element of REAL
y99 *' x99 is Element of REAL+
j is Element of REAL
x is Element of REAL
y is Element of REAL+
z is Element of REAL+
y *' z is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
y9 *' z9 is Element of REAL+
y is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y *' z is Element of REAL+
[0,(y *' z)] is non empty set
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 *' z9 is Element of REAL+
[0,(y9 *' z9)] is non empty set
y is Element of REAL+
[0,y] is non empty set
z is Element of REAL+
z *' y is Element of REAL+
[0,(z *' y)] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
z9 *' y9 is Element of REAL+
[0,(z9 *' y9)] is non empty set
y is Element of REAL+
[0,y] is non empty set
z is Element of REAL+
[0,z] is non empty set
z *' y is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
z9 *' y9 is Element of REAL+
x is Element of REAL+
y is Element of REAL+
j is Element of REAL
x *' y is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z *' y9 is Element of REAL+
[0,(z *' y9)] is non empty set
x9 is Element of REAL+
yz9 is Element of REAL+
z9 is Element of REAL
x9 *' yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
y99 *' x99 is Element of REAL+
[0,(y99 *' x99)] is non empty set
z99 is Element of REAL+
zy9 is Element of REAL+
xy99 is Element of REAL
z99 *' zy9 is Element of REAL+
c16 is Element of REAL+
[0,c16] is non empty set
c17 is Element of REAL+
[0,c17] is non empty set
c17 *' c16 is Element of REAL+
c19 is Element of REAL+
c20 is Element of REAL+
[0,c20] is non empty set
c18 is Element of REAL
c19 *' c20 is Element of REAL+
[0,(c19 *' c20)] is non empty set
c21 is Element of REAL+
[0,c21] is non empty set
c22 is Element of REAL+
c22 *' c21 is Element of REAL+
[0,(c22 *' c21)] is non empty set
c24 is Element of REAL+
c25 is Element of REAL+
[0,c25] is non empty set
c23 is Element of REAL
c24 *' c25 is Element of REAL+
[0,(c24 *' c25)] is non empty set
c26 is Element of REAL+
[0,c26] is non empty set
c27 is Element of REAL+
[0,c27] is non empty set
c27 *' c26 is Element of REAL+
c29 is Element of REAL+
[0,c29] is non empty set
c30 is Element of REAL+
c28 is Element of REAL
c30 *' c29 is Element of REAL+
[0,(c30 *' c29)] is non empty set
c31 is Element of REAL+
[0,c31] is non empty set
c32 is Element of REAL+
[0,c32] is non empty set
c32 *' c31 is Element of REAL+
x is Element of REAL
y is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
j is Element of REAL
z *' y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 *' yz9 is Element of REAL+
[0,(x99 *' yz9)] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
xy99 *' y99 is Element of REAL+
RR is Element of REAL
REAL+ \/ is non empty set
(RR,RR) is Element of REAL
j is Element of REAL+
j + j is Element of REAL+
[0,RR] is non empty set
[0,0] is non empty set
x is Element of REAL+
j is Element of REAL
(RR,j) is Element of REAL
o is Element of REAL+
o + x is Element of REAL+
x -' x is Element of REAL+
x - x is set
j is set
x is set
[j,x] is non empty set
y is Element of REAL
(RR,y) is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 - z9 is set
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 - x9 is set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 - yz9 is set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
xy99 + y99 is Element of REAL+
[0,(xy99 + y99)] is non empty set
o is Element of REAL
(RR,o) is Element of REAL
j is Element of REAL
(RR,j) is Element of REAL
x is Element of REAL+
y is Element of REAL+
x + y is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
x is Element of REAL+
y is Element of REAL+
[0,y] is non empty set
x - y is set
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
[0,0] is non empty set

x is Element of REAL+
y is Element of REAL+
[0,y] is non empty set
x - y is set
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
[0,0] is non empty set

x is Element of REAL+
y is Element of REAL+
[0,y] is non empty set
x - y is set
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z - y9 is set
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
y - x is set
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
y9 - z is set
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
[0,y] is non empty set
x + y is Element of REAL+
[0,(x + y)] is non empty set
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
[0,y] is non empty set
x + y is Element of REAL+
[0,(x + y)] is non empty set
j is Element of REAL
o is Element of REAL
(j,o) is Element of REAL
(o,j) is Element of REAL
REAL+ \/ is non empty set
o is Element of REAL+
j is Element of REAL+
o *' j is Element of REAL+
x is Element of REAL
(RR,x) is Element of REAL
[0,0] is non empty set

o is set
j is set
[o,j] is non empty set
x is Element of REAL+
y is Element of REAL+
x *' y is Element of REAL+
[0,y] is non empty set
z is Element of REAL
(RR,z) is Element of REAL
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
z9 *' y9 is Element of REAL+
o is Element of REAL
(RR,o) is Element of REAL
j is Element of REAL
(RR,j) is Element of REAL
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
REAL+ \/ is non empty set
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
x is Element of REAL+
y is Element of REAL+
x *' y is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
[0,y] is non empty set
y *' x is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
x is Element of REAL+
y is Element of REAL+
[0,y] is non empty set
x *' y is Element of REAL+
[0,(x *' y)] is non empty set
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
y *' x is Element of REAL+
[0,(y *' x)] is non empty set
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
y *' x is Element of REAL+
[0,(y *' x)] is non empty set
x is Element of REAL+
y is Element of REAL+
[0,y] is non empty set
x *' y is Element of REAL+
[0,(x *' y)] is non empty set
j is Element of REAL
o is Element of REAL
(j,o) is Element of REAL
(o,j) is Element of REAL
REAL+ \/ is non empty set
x is Element of REAL+
y is Element of REAL+
x *' y is Element of REAL+
RR is set
o is set
[RR,o] is non empty set
j is set
{j} is non empty trivial set
{RR} is non empty trivial set
{RR,o} is non empty set
{{RR,o},{RR}} is non empty set
RR is Element of REAL
o is Element of REAL
(0,1) --> (RR,o) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
{0,1} is non empty set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set
[0,RR] is non empty set
[1,o] is non empty set
{[0,RR],[1,o]} is non empty set
y is set
z is set
[y,z] is non empty set
{0,z} is non empty set
{{0,z},} is non empty set
{1,o} is non empty set
{1} is non empty trivial set
{{1,o},{1}} is non empty set
{1,o} is non empty set
{1} is non empty trivial set
{{1,o},{1}} is non empty set
{1,o} is non empty set
{1} is non empty trivial set
{{1,o},{1}} is non empty set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : ( b1,b2 are_relative_prime & not b2 = {} ) } is set

[y,z] is non empty set
{y,z} is non empty set
{y} is non empty trivial set
{{y,z},{y}} is non empty set
{{y}} is non empty trivial set
{1,o} is non empty set
{1} is non empty trivial set
{{1,o},{1}} is non empty set
{0,RR} is non empty set
{{0,RR},} is non empty set
{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of NAT : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
y is set
[0,y] is non empty set
z is set
[1,z] is non empty set
{[0,y],[1,z]} is non empty set
y9 is Element of bool RAT+
z9 is Element of RAT+
x9 is Element of RAT+
z9 is Element of RAT+
x9 is Element of RAT+
yz9 is Element of RAT+
o is Element of REAL
RR is Element of REAL
(0,1) --> (RR,o) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
{0,1} is non empty set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set
Funcs ({0,1},REAL) is functional non empty FUNCTION_DOMAIN of {0,1}, REAL
{ b1 where b1 is Relation-like Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is set

x . 1 is set
(Funcs ({0,1},REAL)) \ { b1 where b1 is Relation-like Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is functional Element of bool (Funcs ({0,1},REAL))
bool (Funcs ({0,1},REAL)) is set
RR is Element of COMPLEX
o is Element of REAL
j is Element of REAL
(o,j) is Element of COMPLEX
Funcs ({0,1},REAL) is functional non empty FUNCTION_DOMAIN of {0,1}, REAL
{ b1 where b1 is Relation-like Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is set
(Funcs ({0,1},REAL)) \ { b1 where b1 is Relation-like Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is functional Element of bool (Funcs ({0,1},REAL))
bool (Funcs ({0,1},REAL)) is set

dom o is set
rng o is set
o . 1 is set
o . 0 is set
j is Element of REAL
x is Element of REAL
(j,x) is Element of COMPLEX
(0,1) --> (j,x) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
((0,1) --> (j,x)) . 1 is set
RR is Element of REAL
o is Element of REAL
(RR,o) is Element of COMPLEX
j is Element of REAL
x is Element of REAL
(j,x) is Element of COMPLEX
(0,1) --> (j,x) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
(0,1) --> (RR,o) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
(0,1) --> (j,x) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
[0,0] is non empty set

y is Element of REAL
x is Element of REAL
(x,y) is Element of REAL
z is Element of REAL+
j is Element of REAL+
z + j is Element of REAL+
REAL+ \/ is non empty set
z is set
y9 is set
[z,y9] is non empty set
j is Element of REAL+
z9 is Element of REAL+
j - z9 is set
x is Element of REAL
j is Element of REAL
(j,x) is Element of REAL
y is Element of REAL+
z is Element of REAL+
y *' z is Element of REAL+
j is Element of REAL
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
(j,(x,y)) is Element of REAL
(j,x) is Element of REAL
((j,x),y) is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
z9 *' x9 is Element of REAL+
yz9 is Element of REAL+
x99 is Element of REAL+
yz9 *' x99 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
y9 *' z is Element of REAL+
[0,(y9 *' z)] is non empty set
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
yz9 *' x99 is Element of REAL+
[0,(yz9 *' x99)] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
xy99 *' y99 is Element of REAL+
[0,(xy99 *' y99)] is non empty set
z *' y9 is Element of REAL+
z9 *' (z *' y9) is Element of REAL+
[0,(z9 *' (z *' y9))] is non empty set
(yz9 *' x99) *' xy99 is Element of REAL+
[0,((yz9 *' x99) *' xy99)] is non empty set
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 *' yz9 is Element of REAL+
[0,(x99 *' yz9)] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
xy99 *' y99 is Element of REAL+
[0,(xy99 *' y99)] is non empty set
yz9 *' x99 is Element of REAL+
(yz9 *' x99) *' xy99 is Element of REAL+
[0,((yz9 *' x99) *' xy99)] is non empty set
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
x99 *' yz9 is Element of REAL+
z9 *' x9 is Element of REAL+
yz9 *' (z9 *' x9) is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z *' y9 is Element of REAL+
[0,(z *' y9)] is non empty set
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
yz9 *' x99 is Element of REAL+
[0,(yz9 *' x99)] is non empty set
yz9 *' (z9 *' x9) is Element of REAL+
[0,(yz9 *' (z9 *' x9))] is non empty set
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
x99 *' yz9 is Element of REAL+
(z9 *' x9) *' x99 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
y9 *' z is Element of REAL+
[0,(y9 *' z)] is non empty set
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
x99 *' yz9 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
xy99 *' y99 is Element of REAL+
yz9 *' (z9 *' x9) is Element of REAL+
z *' y9 is Element of REAL+
(z *' y9) *' xy99 is Element of REAL+
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
(y,x) is Element of REAL
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
x99 *' yz9 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 *' xy99 is Element of REAL+
[0,(y99 *' xy99)] is non empty set
o is Element of REAL
(o,y) is Element of REAL
o is Element of REAL
(j,o) is Element of REAL
(o,y) is Element of REAL
o is Element of REAL
(j,o) is Element of REAL
is non empty set

() \/ () is set
REAL+ \/ () is non empty set
j is Element of REAL
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
(j,(x,y)) is Element of REAL
(j,x) is Element of REAL
(j,y) is Element of REAL
((j,x),(j,y)) is Element of REAL
o is Element of REAL
(o,o) is Element of REAL
((j,x),o) is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
z9 *' x9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
z *' y9 is Element of REAL+
z9 is Element of REAL+
x9 is Element of REAL+
z9 *' x9 is Element of REAL+
yz9 is Element of REAL+
x99 is Element of REAL+
yz9 *' x99 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
y99 + xy99 is Element of REAL+
z99 is Element of REAL+
zy9 is Element of REAL+
z99 + zy9 is Element of REAL+
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z - y9 is set
z9 is Element of REAL+
x9 is Element of REAL+
z9 *' x9 is Element of REAL+
yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
yz9 *' x99 is Element of REAL+
[0,(yz9 *' x99)] is non empty set
z -' y9 is Element of REAL+
(z9 *' x9) - (yz9 *' x99) is set
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 - xy99 is set
y9 -' z is Element of REAL+
[0,(y9 -' z)] is non empty set
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 *' xy99 is Element of REAL+
[0,(y99 *' xy99)] is non empty set
y99 *' (y9 -' z) is Element of REAL+
[0,(y99 *' (y9 -' z))] is non empty set
(z9 *' x9) - (yz9 *' x99) is set
z99 is Element of REAL+
zy9 is Element of REAL+
[0,zy9] is non empty set
z99 - zy9 is set
(y,x) is Element of REAL
z is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z - y9 is set
z9 is Element of REAL+
x9 is Element of REAL+
z9 *' x9 is Element of REAL+
yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
yz9 *' x99 is Element of REAL+
[0,(yz9 *' x99)] is non empty set
((j,y),(j,x)) is Element of REAL
z -' y9 is Element of REAL+
(j,(y,x)) is Element of REAL
(z9 *' x9) - (yz9 *' x99) is set
y99 is Element of REAL+
xy99 is Element of REAL+
y99 *' xy99 is Element of REAL+
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 - xy99 is set
y9 -' z is Element of REAL+
[0,(y9 -' z)] is non empty set
(j,(y,x)) is Element of REAL
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 *' xy99 is Element of REAL+
[0,(y99 *' xy99)] is non empty set
y99 *' (y9 -' z) is Element of REAL+
[0,(y99 *' (y9 -' z))] is non empty set
(z9 *' x9) - (yz9 *' x99) is set
z99 is Element of REAL+
zy9 is Element of REAL+
[0,zy9] is non empty set
z99 - zy9 is set
(j,(y,x)) is Element of REAL
(j,(y,x)) is Element of REAL
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
z + y9 is Element of REAL+
[0,(z + y9)] is non empty set
z9 is Element of REAL+
x9 is Element of REAL+
[0,x9] is non empty set
z9 *' x9 is Element of REAL+
[0,(z9 *' x9)] is non empty set
yz9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
yz9 *' x99 is Element of REAL+
[0,(yz9 *' x99)] is non empty set
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 *' xy99 is Element of REAL+
[0,(y99 *' xy99)] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
[0,zy9] is non empty set
z99 + zy9 is Element of REAL+
[0,(z99 + zy9)] is non empty set
z9 *' (z + y9) is Element of REAL+
[0,(z9 *' (z + y9))] is non empty set
yz9 *' xy99 is Element of REAL+
(yz9 *' x99) + (yz9 *' xy99) is Element of REAL+
[0,((yz9 *' x99) + (yz9 *' xy99))] is non empty set
z is Element of REAL+
y9 is Element of REAL+
z + y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 *' yz9 is Element of REAL+
[0,(x99 *' yz9)] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
xy99 *' y99 is Element of REAL+
[0,(xy99 *' y99)] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
[0,zy9] is non empty set
z99 + zy9 is Element of REAL+
[0,(z99 + zy9)] is non empty set
y99 *' xy99 is Element of REAL+
z9 *' x9 is Element of REAL+
(y99 *' xy99) + (z9 *' x9) is Element of REAL+
[0,((y99 *' xy99) + (z9 *' x9))] is non empty set
o is Element of REAL
(o,o) is Element of REAL
((j,x),o) is Element of REAL
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 - yz9 is set
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 - xy99 is set
y99 -' xy99 is Element of REAL+
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
zy9 *' z99 is Element of REAL+
[0,(zy9 *' z99)] is non empty set
z9 *' y9 is Element of REAL+
z9 *' x9 is Element of REAL+
(z9 *' y9) - (z9 *' x9) is set
z9 *' x9 is Element of REAL+
xy99 -' y99 is Element of REAL+
[0,(xy99 -' y99)] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
[0,zy9] is non empty set
zy9 *' z99 is Element of REAL+
z99 *' (xy99 -' y99) is Element of REAL+
z *' y9 is Element of REAL+
z9 *' x9 is Element of REAL+
(z *' y9) - (z9 *' x9) is set
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
y9 *' z is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
x9 *' z9 is Element of REAL+
[0,(x9 *' z9)] is non empty set
((j,y),(j,x)) is Element of REAL
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
x99 - yz9 is set
(y,x) is Element of REAL
y99 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
y99 - xy99 is set
y99 -' xy99 is Element of REAL+
(j,(y,x)) is Element of REAL
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
zy9 *' z99 is Element of REAL+
[0,(zy9 *' z99)] is non empty set
z9 *' y9 is Element of REAL+
z9 *' x9 is Element of REAL+
(z9 *' y9) - (z9 *' x9) is set
z9 *' x9 is Element of REAL+
(j,(y,x)) is Element of REAL
(j,(y,x)) is Element of REAL
(j,(y,x)) is Element of REAL
xy99 -' y99 is Element of REAL+
[0,(xy99 -' y99)] is non empty set
(j,(y,x)) is Element of REAL
z99 is Element of REAL+
[0,z99] is non empty set
zy9 is Element of REAL+
[0,zy9] is non empty set
zy9 *' z99 is Element of REAL+
z99 *' (xy99 -' y99) is Element of REAL+
z *' y9 is Element of REAL+
z9 *' x9 is Element of REAL+
(z *' y9) - (z9 *' x9) is set
z is Element of REAL+
[0,z] is non empty set
y9 is Element of REAL+
[0,y9] is non empty set
z + y9 is Element of REAL+
[0,(z + y9)] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
x9 is Element of REAL+
[0,x9] is non empty set
x9 *' z9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
x99 *' yz9 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
xy99 *' y99 is Element of REAL+
y99 *' (z + y9) is Element of REAL+
z99 is Element of REAL+
zy9 is Element of REAL+
z99 + zy9 is Element of REAL+

() \/ () is set
REAL+ \/ () is non empty set
j is Element of REAL
(j) is Element of REAL
x is Element of REAL
((j),x) is Element of REAL
(j,x) is Element of REAL
((j,x)) is Element of REAL
(((j),x),(j,x)) is Element of REAL
((j),j) is Element of REAL
(((j),j),x) is Element of REAL
o is Element of REAL
(o,x) is Element of REAL
j is Element of REAL
(j,j) is Element of REAL
REAL+ \/ is non empty set
x is Element of REAL+
y is Element of REAL+
x *' y is Element of REAL+
x is Element of REAL+
[0,x] is non empty set
y is Element of REAL+
[0,y] is non empty set
y *' x is Element of REAL+
j is Element of REAL
(j,j) is Element of REAL
x is Element of REAL
(x,x) is Element of REAL
((j,j),(x,x)) is Element of REAL
y is Element of REAL+
z is Element of REAL+
y + z is Element of REAL+
REAL+ \/ is non empty set
y9 is Element of REAL+
z9 is Element of REAL+
y9 *' z9 is Element of REAL+
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
z9 *' y9 is Element of REAL+
j is Element of REAL
x is Element of REAL
(j,x) is Element of REAL
y is Element of REAL
(j,y) is Element of REAL
(j) is Element of REAL
j is Element of REAL
x is Element of REAL
(j,x) is Element of REAL
(j) is Element of REAL
(j,(j)) is Element of REAL
(x,x) is Element of REAL
((j,x),(j)) is Element of REAL
((j,(j)),x) is Element of REAL
y is Element of REAL+
z is Element of REAL+
y *' z is Element of REAL+
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
(y) is Element of REAL
((x,y),(y)) is Element of REAL
(y,(y)) is Element of REAL
(x,(y,(y))) is Element of REAL
j is Element of REAL
(x,j) is Element of REAL
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
(x) is Element of REAL
(x,(x)) is Element of REAL
j is Element of REAL
(j,y) is Element of REAL
((x,y),(x)) is Element of REAL
x is Element of REAL
(x) is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
((x,y)) is Element of REAL
(y) is Element of REAL
((x),(y)) is Element of REAL
(x,(x)) is Element of REAL
(y,(y)) is Element of REAL
((x,y),((x),(y))) is Element of REAL
((x,y),(x)) is Element of REAL
(((x,y),(x)),(y)) is Element of REAL
j is Element of REAL
(j,y) is Element of REAL
((j,y),(y)) is Element of REAL
x is Element of REAL
y is Element of REAL
z is Element of REAL
(y,z) is Element of REAL
(x,(y,z)) is Element of REAL
(x,y) is Element of REAL
((x,y),z) is Element of REAL
REAL+ \/ is non empty set
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
x9 is Element of REAL+
yz9 is Element of REAL+
x9 + yz9 is Element of REAL+
x99 is Element of REAL+
y99 is Element of REAL+
x99 + y99 is Element of REAL+
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 - z9 is set
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 - yz9 is set
x9 -' yz9 is Element of REAL+
x99 is Element of REAL+
y99 is Element of REAL+
x99 + y99 is Element of REAL+
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
yz9 -' x9 is Element of REAL+
[0,(yz9 -' x9)] is non empty set
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
x99 - (yz9 -' x9) is set
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 - z9 is set
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 - yz9 is set
x9 -' yz9 is Element of REAL+
x99 is Element of REAL+
y99 is Element of REAL+
x99 + y99 is Element of REAL+
x99 -' yz9 is Element of REAL+
(z,(x,y)) is Element of REAL
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
y9 -' yz9 is Element of REAL+
(z,(x,y)) is Element of REAL
yz9 -' x9 is Element of REAL+
[0,(yz9 -' x9)] is non empty set
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
x99 - (yz9 -' x9) is set
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
(y,x) is Element of REAL
yz9 -' y9 is Element of REAL+
[0,(yz9 -' y9)] is non empty set
(z,(y,x)) is Element of REAL
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
(z,y) is Element of REAL
x9 -' yz9 is Element of REAL+
(x,(z,y)) is Element of REAL
x99 - (yz9 -' y9) is set
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
yz9 -' x9 is Element of REAL+
[0,(yz9 -' x9)] is non empty set
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
(y,x) is Element of REAL
yz9 -' y9 is Element of REAL+
[0,(yz9 -' y9)] is non empty set
(z,(y,x)) is Element of REAL
xy99 is Element of REAL+
z99 is Element of REAL+
[0,z99] is non empty set
xy99 - z99 is set
x99 - (yz9 -' x9) is set
xy99 - (yz9 -' y9) is set
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
y9 + z9 is Element of REAL+
[0,(y9 + z9)] is non empty set
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 - yz9 is set
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
x99 -' y99 is Element of REAL+
xy99 is Element of REAL+
z99 is Element of REAL+
[0,z99] is non empty set
xy99 - z99 is set
x9 - (y9 + z9) is set
y99 -' x99 is Element of REAL+
[0,(y99 -' x99)] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
xy99 + z99 is Element of REAL+
[0,(xy99 + z99)] is non empty set
z9 + y9 is Element of REAL+
(z9 + y9) -' x9 is Element of REAL+
[0,((z9 + y9) -' x9)] is non empty set
z99 + (y99 -' x99) is Element of REAL+
[0,(z99 + (y99 -' x99))] is non empty set
(z,y) is Element of REAL
((z,y),x) is Element of REAL
y9 is Element of REAL+
z9 is Element of REAL+
y9 + z9 is Element of REAL+
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 - z9 is set
(y,x) is Element of REAL
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 - yz9 is set
x9 -' yz9 is Element of REAL+
(z,(y,x)) is Element of REAL
x99 is Element of REAL+
y99 is Element of REAL+
x99 + y99 is Element of REAL+
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
yz9 -' x9 is Element of REAL+
[0,(yz9 -' x9)] is non empty set
(z,(y,x)) is Element of REAL
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
x99 - (yz9 -' x9) is set
xy99 is Element of REAL+
z99 is Element of REAL+
xy99 + z99 is Element of REAL+
(z,(y,x)) is Element of REAL
(z,(y,x)) is Element of REAL
y9 is Element of REAL+
z9 is Element of REAL+
[0,z9] is non empty set
y9 - z9 is set
x9 is Element of REAL+
[0,x9] is non empty set
yz9 is Element of REAL+
yz9 - x9 is set
y9 -' z9 is Element of REAL+
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
y99 - x99 is set
y9 -' x99 is Element of REAL+
(z,(x,y)) is Element of REAL
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
z99 - xy99 is set
(y,x) is Element of REAL
x9 -' yz9 is Element of REAL+
[0,(x9 -' yz9)] is non empty set
(z,(y,x)) is Element of REAL
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
x99 + y99 is Element of REAL+
[0,(x99 + y99)] is non empty set
y9 -' z9 is Element of REAL+
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
z99 - xy99 is set
xy99 -' (y9 -' z9) is Element of REAL+
[0,(xy99 -' (y9 -' z9))] is non empty set
(x9 -' yz9) + x99 is Element of REAL+
[0,((x9 -' yz9) + x99)] is non empty set
(z,y) is Element of REAL
z9 -' y9 is Element of REAL+
[0,(z9 -' y9)] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
x99 + y99 is Element of REAL+
[0,(x99 + y99)] is non empty set
(y,x) is Element of REAL
yz9 -' x9 is Element of REAL+
(z,(y,x)) is Element of REAL
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
z99 - xy99 is set
(z9 -' y9) + x99 is Element of REAL+
[0,((z9 -' y9) + x99)] is non empty set
xy99 -' (yz9 -' x9) is Element of REAL+
[0,(xy99 -' (yz9 -' x9))] is non empty set
(z,y) is Element of REAL
(y,x) is Element of REAL
x9 -' yz9 is Element of REAL+
[0,(x9 -' yz9)] is non empty set
(z,(y,x)) is Element of REAL
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
x99 + y99 is Element of REAL+
[0,(x99 + y99)] is non empty set
z9 -' y9 is Element of REAL+
[0,(z9 -' y9)] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
xy99 + z99 is Element of REAL+
[0,(xy99 + z99)] is non empty set
(z9 -' y9) + xy99 is Element of REAL+
[0,((z9 -' y9) + xy99)] is non empty set
(x9 -' yz9) + x99 is Element of REAL+
[0,((x9 -' yz9) + x99)] is non empty set
(y,x) is Element of REAL
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
y9 + z9 is Element of REAL+
[0,(y9 + z9)] is non empty set
(z,(y,x)) is Element of REAL
x9 is Element of REAL+
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 - yz9 is set
(z,y) is Element of REAL
x99 is Element of REAL+
y99 is Element of REAL+
[0,y99] is non empty set
x99 - y99 is set
x99 -' y99 is Element of REAL+
((z,y),x) is Element of REAL
xy99 is Element of REAL+
z99 is Element of REAL+
[0,z99] is non empty set
xy99 - z99 is set
x9 - (y9 + z9) is set
y99 -' x99 is Element of REAL+
[0,(y99 -' x99)] is non empty set
((z,y),x) is Element of REAL
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
xy99 + z99 is Element of REAL+
[0,(xy99 + z99)] is non empty set
z9 + y9 is Element of REAL+
(z9 + y9) -' x9 is Element of REAL+
[0,((z9 + y9) -' x9)] is non empty set
z99 + (y99 -' x99) is Element of REAL+
[0,(z99 + (y99 -' x99))] is non empty set
((z,y),x) is Element of REAL
((z,y),x) is Element of REAL
(z,y) is Element of REAL
y9 is Element of REAL+
[0,y9] is non empty set
z9 is Element of REAL+
[0,z9] is non empty set
y9 + z9 is Element of REAL+
[0,(y9 + z9)] is non empty set
x9 is Element of REAL+
[0,x9] is non empty set
yz9 is Element of REAL+
[0,yz9] is non empty set
x9 + yz9 is Element of REAL+
[0,(x9 + yz9)] is non empty set
x99 is Element of REAL+
[0,x99] is non empty set
y99 is Element of REAL+
[0,y99] is non empty set
x99 + y99 is Element of REAL+
[0,(x99 + y99)] is non empty set
xy99 is Element of REAL+
[0,xy99] is non empty set
z99 is Element of REAL+
[0,z99] is non empty set
xy99 + z99 is Element of REAL+
[0,(xy99 + z99)] is non empty set
z9 + y9 is Element of REAL+
(z9 + y9) + x9 is Element of REAL+
[0,((z9 + y9) + x9)] is non empty set
y99 + x99 is Element of REAL+
z99 + (y99 + x99) is Element of REAL+
[0,(z99 + (y99 + x99))] is non empty set
x is Element of REAL
y is Element of REAL
(x,y) is Element of COMPLEX
(0,1) --> (x,y) is Relation-like NAT -defined Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
x is Element of REAL
y is Element of REAL
(x,y) is Element of REAL
((x,y)) is Element of REAL
(x) is Element of REAL
(y) is Element of REAL
((x),(y)) is Element of REAL
((x,y),((x),(y))) is Element of REAL
(y,((x),(y))) is Element of REAL
(x,(y,((x),(y)))) is Element of REAL
(y,(y)) is Element of REAL
((x),(y,(y))) is Element of REAL
(x,((x),(y,(y)))) is Element of REAL
o is Element of REAL
((x),o) is Element of REAL
(x,((x),o)) is Element of REAL
(x,(x)) is Element of REAL