:: ARYTM_0 semantic presentation

REAL is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is set

omega is non empty epsilon-transitive epsilon-connected ordinal set

RAT+ is set

{} is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

{ [b

1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of NAT

{ [b

{ [b

bool { [b

( { [b

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+

{ b

( not b

( not b

( b

{RAT+} is non empty trivial set

{ b

( not b

( not b

( b

( not b

( not b

( b

bool { b

( not b

( not b

( b

RAT+ \/ DEDEKIND_CUTS is non empty set

{ { b

(RAT+ \/ DEDEKIND_CUTS) \ { { b

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

{ b

(Funcs ({{},1},REAL)) \ { b

bool (Funcs ({{},1},REAL)) is set

((Funcs ({{},1},REAL)) \ { b

{{}} 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

c

[0,c

c

c

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+

c

[0,c

c

[0,c

c

c

c

[0,c

c

c

[0,(c

c

[0,c

c

c

[0,(c

c

c

[0,c

c

c

[0,(c

c

[0,c

c

[0,c

c

c

[0,c

c

c

c

[0,(c

c

[0,c

c

[0,c

c

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

{ [b

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

{ [b

{ [b

bool { [b

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

{ b

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)) \ { b

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

{ b

(Funcs ({0,1},REAL)) \ { b

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