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
RAT+ is set
{} is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural 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
1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of NAT
{ [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 RAT+ is set
bool (bool RAT+) is set
DEDEKIND_CUTS is non empty Element of bool (bool RAT+)
REAL+ is non empty set
{} is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of RAT+
{ 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+} 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 ) ) ) } \ {RAT+} 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
(RAT+ \/ DEDEKIND_CUTS) \ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is Element of bool (RAT+ \/ DEDEKIND_CUTS)
bool (RAT+ \/ DEDEKIND_CUTS) is set
one is non empty epsilon-transitive epsilon-connected ordinal Element of RAT+
{{}} is non empty trivial set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is non empty set
[{},{}] is non empty set
{[{},{}]} is Function-like non empty trivial set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) 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 set
REAL+ \/ [:{{}},REAL+:] is non empty set
RR is Element of REAL+
[{},RR] is non empty set
[{},{}] is non empty set
{[{},{}]} is Function-like non empty trivial set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is non empty set
RR is set
[{},RR] is non empty set
[{},{}] is non empty set
{[{},{}]} is Function-like non empty trivial 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
[:{{}},REAL+:] is 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
0 is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of NAT
{0} is non empty trivial set
[:{0},REAL+:] is 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+ \/ [:{0},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+ \/ [:{0},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
{[0,0]} is Function-like non empty trivial 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
{[0,0]} is Function-like non empty trivial 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+ \/ [:{0},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
{[0,0]} is Function-like non empty trivial 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+ \/ [:{0},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+ \/ [:{0},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},{0}} 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 is epsilon-transitive epsilon-connected ordinal natural Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural Element of NAT
[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},{0}} 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 is Relation-like Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL)
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
o is Relation-like Function-like 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
{[0,0]} is Function-like non empty trivial set
[:{0},REAL+:] \ {[0,0]} is Element of bool [:{0},REAL+:]
bool [:{0},REAL+:] is 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+ \/ [:{{}},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 Function-like non empty trivial set
REAL+ \ {[{},{}]} is Element of bool REAL+
bool REAL+ is set
[:{{}},REAL+:] \ {[{},{}]} is Element of bool [:{{}},REAL+:]
bool [:{{}},REAL+:] is set
(REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) is set
REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) 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+
REAL+ \ {[0,0]} is Element of bool REAL+
bool REAL+ is set
(REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) is set
REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) 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+ \/ [:{{}},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+ \/ [:{{}},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+ \/ [:{0},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