:: ARYTM_1 semantic presentation

K27() is set
RAT+ is set
K6(RAT+) is set
K6(K6(RAT+)) is set
DEDEKIND_CUTS is Element of K6(K6(RAT+))
REAL+ is set
{} is Element of RAT+
one is V1() V6() Element of RAT+
u is Element of REAL+
y is Element of REAL+
u + y is Element of REAL+
z is Element of REAL+
y + z 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 *' x is Element of REAL+
z0 is Element of REAL+
y *' z0 is Element of REAL+
(y *' z0) *' z is Element of REAL+
z0 *' (y *' x) is Element of REAL+
(y *' z0) *' 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 *' x is Element of REAL+
(y *' x) *' z is Element of REAL+
(y *' z) *' x is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
z0 is Element of REAL+
y + z0 is Element of REAL+
x1 is Element of REAL+
z + x1 is Element of REAL+
z0 + x1 is Element of REAL+
y + (z0 + x1) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
y + x is Element of REAL+
z0 is Element of REAL+
z + z0 is Element of REAL+
x + z0 is Element of REAL+
y + (x + z0) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
y + x is Element of REAL+
y is Element of REAL+
z is Element of REAL+
y + z is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
y + x is Element of REAL+
z + x is Element of REAL+
z0 is Element of REAL+
y + z0 is Element of REAL+
(y + x) + z0 is Element of REAL+
z0 is Element of REAL+
(y + x) + z0 is Element of REAL+
y + z0 is Element of REAL+
(y + z0) + x is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
y *' x is Element of REAL+
z *' x is Element of REAL+
z0 is Element of REAL+
y + z0 is Element of REAL+
z0 *' x is Element of REAL+
(y *' x) + (z0 *' 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 *' x is Element of REAL+
z0 is Element of REAL+
(y *' z) + z0 is Element of REAL+
x1 is Element of REAL+
y *' x1 is Element of REAL+
u is Element of REAL+
u *' z0 is Element of REAL+
(y *' z) + (u *' z0) is Element of REAL+
x1 *' z0 is Element of REAL+
y *' (x1 *' z0) is Element of REAL+
(y *' z) + (y *' (x1 *' z0)) is Element of REAL+
z + (x1 *' z0) is Element of REAL+
y *' (z + (x1 *' z0)) is Element of REAL+
z is Element of REAL+
y is Element of REAL+
x is Element of REAL+
z + x is Element of REAL+
z0 is Element of REAL+
z0 + z is Element of REAL+
x1 is Element of REAL+
x1 + z is Element of REAL+
c₇ is Element of REAL+
c₈ is Element of REAL+
y is Element of REAL+
(y,y) is Element of REAL+
(y,y) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(y,z) is Element of REAL+
(y,z) + z is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(y,z) is Element of REAL+
(y,z) + z is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
(z,y) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
y + z is Element of REAL+
((y + z),z) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
(z,(z,y)) is Element of REAL+
(z,(z,y)) + (z,y) is Element of REAL+
(z,y) + y 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+
x + z is Element of REAL+
(y,z) + z is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
x + y is Element of REAL+
(z,y) + y 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,z),x) is Element of REAL+
x + z is Element of REAL+
(y,(x + z)) is Element of REAL+
((y,z),x) + (x + z) is Element of REAL+
((y,z),x) + x is Element of REAL+
(((y,z),x) + x) + z is Element of REAL+
(y,z) + z is Element of REAL+
z + 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,z),x) is Element of REAL+
(y,x) is Element of REAL+
((y,x),z) is Element of REAL+
x + z is Element of REAL+
(y,(x + z)) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(x,y) is Element of REAL+
z + (x,y) is Element of REAL+
(z,y) + x is Element of REAL+
(z + (x,y)) + y is Element of REAL+
(x,y) + y is Element of REAL+
z + ((x,y) + y) is Element of REAL+
z + x is Element of REAL+
(z,y) + y is Element of REAL+
((z,y) + y) + x is Element of REAL+
((z,y) + x) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
x + (z,y) is Element of REAL+
x + z is Element of REAL+
((x + z),y) is Element of REAL+
(x + (z,y)) + y is Element of REAL+
(z,y) + y is Element of REAL+
x + ((z,y) + y) is Element of REAL+
((x + z),y) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(x,(z,y)) is Element of REAL+
x + y is Element of REAL+
((x + y),z) is Element of REAL+
(x,(z,y)) + (z,y) is Element of REAL+
x + z is Element of REAL+
((x + z),z) is Element of REAL+
y + (z,y) is Element of REAL+
x + (y + (z,y)) is Element of REAL+
((x + (y + (z,y))),z) is Element of REAL+
(x + y) + (z,y) is Element of REAL+
(((x + y) + (z,y)),z) is Element of REAL+
((x + y),z) + (z,y) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(y,x) is Element of REAL+
(z,(y,x)) is Element of REAL+
(z,y) + x is Element of REAL+
z + x is Element of REAL+
((z + x),y) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(z,x) is Element of REAL+
(y,(z,x)) is Element of REAL+
(x,(z,y)) is Element of REAL+
y + x is Element of REAL+
((y + x),z) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(z,y) + x is Element of REAL+
(y,x) is Element of REAL+
(z,(y,x)) is Element of REAL+
z + x is Element of REAL+
((z + x),y) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(x,y) is Element of REAL+
(x,y) + z is Element of REAL+
(z,y) + x is Element of REAL+
((x,y) + z) + y is Element of REAL+
(x,y) + y is Element of REAL+
((x,y) + y) + z is Element of REAL+
x + z is Element of REAL+
(z,y) + y is Element of REAL+
((z,y) + y) + x is Element of REAL+
((z,y) + x) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
(x,z) is Element of REAL+
(x,y) is Element of REAL+
(x,z) + y is Element of REAL+
(x,z) + z is Element of REAL+
(x,y) + y is Element of REAL+
y is Element of REAL+
z is Element of REAL+
x is Element of REAL+
(y,x) is Element of REAL+
(z,x) is Element of REAL+
(z,x) + x is Element of REAL+
(y,x) + 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+
(z,x) is Element of REAL+
y *' (z,x) is Element of REAL+
y *' x is Element of REAL+
((y *' z),(y *' x)) is Element of REAL+
(y *' (z,x)) + (y *' x) is Element of REAL+
(z,x) + x is Element of REAL+
y *' ((z,x) + x) is Element of REAL+
((y *' z),(y *' x)) + (y *' x) is Element of REAL+
z is Element of REAL+
y is Element of REAL+
(y,z) is Element of REAL+
(z,y) is Element of REAL+
[{},(z,y)] is set
y is Element of REAL+
(y,y) is set
(y,y) is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(y,z) is set
[{},z] is set
(z,y) is Element of REAL+
[{},(z,y)] is set
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
x + (z,y) is Element of REAL+
x + z is Element of REAL+
((x + z),y) is set
((x + z),y) 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+
(x,(y,z)) is set
x + z is Element of REAL+
((x + z),y) is set
((x + z),y) is Element of REAL+
(x,(y,z)) is Element of REAL+
((y,z),x) is Element of REAL+
(y,(x + z)) is Element of REAL+
[{},(y,(x + z))] is set
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(y,x) is Element of REAL+
(z,(y,x)) is set
(z,y) + x is Element of REAL+
(z,(y,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,x) is Element of REAL+
(z,(y,x)) is set
(x,(y,z)) is set
z + x is Element of REAL+
(x,(y,z)) is Element of REAL+
(z,(y,x)) is Element of REAL+
z + x is Element of REAL+
((y,x),z) is Element of REAL+
((y,z),x) is Element of REAL+
[{},((y,z),x)] is set
z + x is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
y + x is Element of REAL+
(z,(y + x)) is set
((z,y),x) is set
((z,y),x) is Element of REAL+
(z,(y + x)) is Element of REAL+
z + x is Element of REAL+
((z + x),z) is Element of REAL+
(z,z) is Element of REAL+
(x,(z,z)) is Element of REAL+
(x,(z,y)) is Element of REAL+
[{},(x,(z,y))] is set
((y + x),z) is Element of REAL+
(x,(z,y)) is Element of REAL+
[{},(x,(z,y))] is set
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
(z,x) is Element of REAL+
((z,x),y) is set
((z,y),x) is set
y + x is Element of REAL+
((z,y),x) is Element of REAL+
((z,x),y) is Element of REAL+
y + x is Element of REAL+
(y,x) is Element of REAL+
(y,(y,x)) is Element of REAL+
(y,y) is Element of REAL+
(x,(y,y)) is Element of REAL+
(x,(z,y)) is Element of REAL+
[{},(x,(z,y))] is set
y + x is Element of REAL+
(x,x) is Element of REAL+
(y,(x,x)) is Element of REAL+
(x,y) is Element of REAL+
(x,(x,y)) is Element of REAL+
(x,(z,y)) is Element of REAL+
[{},(x,(z,y))] is set
y + x is Element of REAL+
(y,(z,x)) is Element of REAL+
(x,(z,y)) is Element of REAL+
[{},(x,(z,y))] is set
y + x is Element of REAL+
y is Element of REAL+
z is Element of REAL+
(z,y) is Element of REAL+
x is Element of REAL+
x *' (z,y) is Element of REAL+
x *' z is Element of REAL+
x *' y is Element of REAL+
((x *' z),(x *' y)) is set
((x *' z),(x *' y)) 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+
x *' (y,z) is Element of REAL+
[{},(x *' (y,z))] is set
x *' z is Element of REAL+
x *' y is Element of REAL+
((x *' z),(x *' y)) is set
((x *' y),(x *' z)) is Element of REAL+
[{},((x *' y),(x *' z))] is set
y is Element of REAL+
z is Element of REAL+
(y,z) is Element of REAL+
x is Element of REAL+
x *' z is Element of REAL+
x *' y is Element of REAL+
((x *' z),(x *' y)) is set
x *' (y,z) is Element of REAL+
[{},(x *' (y,z))] is set