:: URYSOHN2 semantic presentation

REAL is non empty V33() V36() complex-membered ext-real-membered real-membered V72() non bounded_below non bounded_above interval set
NAT is V33() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below Element of K32(REAL)
K32(REAL) is non empty set
ExtREAL is non empty ext-real-membered interval set
K33(NAT,ExtREAL) is set
K32(K33(NAT,ExtREAL)) is non empty set
K32(ExtREAL) is non empty set
omega is V33() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below set
K32(omega) is non empty set
K33(NAT,REAL) is set
K32(K33(NAT,REAL)) is non empty set
K32(K32(REAL)) is non empty set
COMPLEX is non empty V36() complex-membered V72() set
K32(NAT) is non empty set
RAT is non empty V36() complex-membered ext-real-membered real-membered rational-membered V72() set
INT is non empty V36() complex-membered ext-real-membered real-membered rational-membered integer-membered V72() set
K33(COMPLEX,COMPLEX) is non empty set
K32(K33(COMPLEX,COMPLEX)) is non empty set
K33(COMPLEX,REAL) is non empty set
K32(K33(COMPLEX,REAL)) is non empty set
1 is non empty ordinal natural V24() real ext-real positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V134() Element of NAT
K33(1,1) is non empty set
K32(K33(1,1)) is non empty set
K33(K33(1,1),1) is non empty set
K32(K33(K33(1,1),1)) is non empty set
K33(K33(1,1),REAL) is non empty set
K32(K33(K33(1,1),REAL)) is non empty set
K33(REAL,REAL) is non empty set
K33(K33(REAL,REAL),REAL) is non empty set
K32(K33(K33(REAL,REAL),REAL)) is non empty set
2 is non empty ordinal natural V24() real ext-real positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V134() Element of NAT
K33(2,2) is non empty set
K33(K33(2,2),REAL) is non empty set
K32(K33(K33(2,2),REAL)) is non empty set
K32(K33(REAL,REAL)) is non empty set
K536(2) is V205() L15()
the U1 of K536(2) is set
K33( the U1 of K536(2),REAL) is set
K32(K33( the U1 of K536(2),REAL)) is non empty set
K32( the U1 of K536(2)) is non empty set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is non empty set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K33(RAT,RAT) is non empty set
K32(K33(RAT,RAT)) is non empty set
K33(K33(RAT,RAT),RAT) is non empty set
K32(K33(K33(RAT,RAT),RAT)) is non empty set
K33(INT,INT) is non empty set
K32(K33(INT,INT)) is non empty set
K33(K33(INT,INT),INT) is non empty set
K32(K33(K33(INT,INT),INT)) is non empty set
K33(NAT,NAT) is set
K33(K33(NAT,NAT),NAT) is set
K32(K33(K33(NAT,NAT),NAT)) is non empty set
0 is empty ordinal natural V24() real ext-real non positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval V134() Element of NAT
the empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
DYADIC is complex-membered ext-real-membered real-membered Element of K32(REAL)
DOM is complex-membered ext-real-membered real-membered Element of K32(REAL)
halfline 0 is complex-membered ext-real-membered real-membered Element of K32(REAL)
-infty is non empty non real ext-real non positive negative set
].-infty,0.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
(halfline 0) \/ DYADIC is complex-membered ext-real-membered real-membered Element of K32(REAL)
right_open_halfline 1 is complex-membered ext-real-membered real-membered Element of K32(REAL)
+infty is non empty non real ext-real positive non negative set
].1,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
K295() is empty ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval Element of ExtREAL
diameter {} is ext-real Element of ExtREAL
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of K32(REAL)
K107(0) is empty V24() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
{+infty,-infty} is non empty ext-real-membered set
REAL \/ {+infty,-infty} is non empty ext-real-membered set
].-infty,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set
eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is ext-real-membered set
eps1 " is V24() real ext-real Element of REAL
(eps1 ") ** (eps1 ** eps) is complex-membered ext-real-membered real-membered Element of K32(REAL)
{(eps1 ")} is non empty complex-membered ext-real-membered real-membered set
{(eps1 ")} ** (eps1 ** eps) is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
{(eps1 ")} ** (eps1 ** eps) is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
(eps1 ") ** (eps1 ** eps) is ext-real-membered set
eps1 is set
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
(eps1 ") * r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
(eps1 ") * eps1 is V24() real ext-real Element of REAL
((eps1 ") * eps1) * r2 is V24() real ext-real Element of REAL
1 * r2 is V24() real ext-real Element of REAL
eps1 is set
d is V24() real ext-real Element of REAL
d / (eps1 ") is V24() real ext-real Element of REAL
K107((eps1 ")) is V24() real ext-real set
K105(d,K107((eps1 "))) is V24() real ext-real set
(eps1 ") * (d / (eps1 ")) is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps1 is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps ** eps1 is complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps} is non empty complex-membered ext-real-membered real-membered set
{eps} ** eps1 is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps} & b₂ in eps1 ) } is set
{eps} ** eps1 is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps} & b₂ in eps1 ) } is set
eps ** eps1 is ext-real-membered set
eps1 is set
d is V24() real ext-real Element of REAL
d / eps is V24() real ext-real Element of REAL
K107(eps) is V24() real ext-real set
K105(d,K107(eps)) is V24() real ext-real set
r1 is V24() real ext-real Element of REAL
eps * r1 is V24() real ext-real Element of REAL
eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
0 ** eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
{0} ** eps is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {0} & b₂ in eps ) } is set
{0} ** eps is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {0} & b₂ in eps ) } is set
0 ** eps is ext-real-membered set
eps1 is set
eps1 is set
d is V24() real ext-real Element of eps
r1 is V24() real ext-real Element of REAL
0 * r1 is V24() real ext-real Element of REAL
eps1 is set
eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
0 * d is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps ** {} is empty proper complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval open_interval Element of K32(REAL)
{eps} is non empty complex-membered ext-real-membered real-membered set
{eps} ** {} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps} & b₂ in {} ) } is set
{eps} ** {} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps} & b₂ in {} ) } is set
eps ** {} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
-infty is non empty non real ext-real non positive negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
eps is ext-real Element of ExtREAL
eps1 is ext-real Element of ExtREAL
{-infty,+infty} is non empty ext-real-membered set
eps is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
0 ** eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
{0} ** eps is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {0} & b₂ in eps ) } is set
{0} ** eps is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {0} & b₂ in eps ) } is set
0 ** eps is ext-real-membered set
[.0,0.] is non empty complex-membered ext-real-membered real-membered interval set
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is ext-real Element of ExtREAL
d is ext-real Element of ExtREAL
].eps1,d.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
].c₇,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
x is ext-real Element of ExtREAL
c₇ is ext-real Element of ExtREAL
].x,c₇.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
(eps1 * r2) / eps1 is V24() real ext-real Element of REAL
K105((eps1 * r2),K107(eps1)) is V24() real ext-real set
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1r1 is ext-real Element of ExtREAL
1o is ext-real Element of ExtREAL
1ra is ext-real Element of ExtREAL
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
].-infty,c₇.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
].-infty,c₇.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
].c₇,x.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
(eps1 * r2) / eps1 is V24() real ext-real Element of REAL
K105((eps1 * r2),K107(eps1)) is V24() real ext-real set
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
1o is V24() real ext-real Element of REAL
1ra is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
1r1 is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
].c₇,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is V24() real ext-real set
d is V24() real ext-real set
[.eps1,d.] is complex-membered ext-real-membered real-membered interval set
r1 is ext-real Element of ExtREAL
r2 is ext-real Element of ExtREAL
c₇ is V24() real ext-real Element of REAL
eps1 * c₇ is V24() real ext-real Element of REAL
x is V24() real ext-real Element of REAL
eps1 * x is V24() real ext-real Element of REAL
q is ext-real Element of ExtREAL
c₉ is ext-real Element of ExtREAL
[.q,c₉.] is ext-real-membered interval set
z2 is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
2r is ext-real Element of ExtREAL
2o1 is ext-real Element of ExtREAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
1o / eps1 is V24() real ext-real Element of REAL
K105(1o,K107(eps1)) is V24() real ext-real set
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
z2 is set
z2 is V24() real ext-real Element of REAL
2o is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
2r is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
1ra is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is ext-real Element of ExtREAL
c₇ is V24() real ext-real Element of REAL
eps1 * c₇ is V24() real ext-real Element of REAL
x is V24() real ext-real Element of REAL
eps1 * x is V24() real ext-real Element of REAL
q is ext-real Element of ExtREAL
c₉ is ext-real Element of ExtREAL
[.q,c₉.] is ext-real-membered interval set
z2 is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
2r is ext-real Element of ExtREAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
2o1 is ext-real Element of ExtREAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
1o / eps1 is V24() real ext-real Element of REAL
K105(1o,K107(eps1)) is V24() real ext-real set
z2 is set
z2 is V24() real ext-real Element of REAL
2o is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
2r is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
1ra is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is V24() real ext-real set
d is ext-real Element of ExtREAL
[.eps1,d.[ is complex-membered ext-real-membered real-membered non right_end interval set
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is V24() real ext-real Element of REAL
eps1 * x is V24() real ext-real Element of REAL
c₉ is ext-real Element of ExtREAL
[.c₉,c₇.[ is ext-real-membered non right_end interval set
q is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
2r is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
q is set
z2 is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1o is ext-real Element of ExtREAL
1ra is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
[.c₇,x.[ is ext-real-membered non right_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is V24() real ext-real set
d is ext-real Element of ExtREAL
[.eps1,d.[ is complex-membered ext-real-membered real-membered non right_end interval set
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is V24() real ext-real Element of REAL
eps1 * x is V24() real ext-real Element of REAL
c₉ is ext-real Element of ExtREAL
].c₇,c₉.] is ext-real-membered non left_end interval set
q is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
2r is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
q is set
z2 is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1o is ext-real Element of ExtREAL
1ra is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
].x,c₇.] is ext-real-membered non left_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is ext-real Element of ExtREAL
d is V24() real ext-real set
].eps1,d.] is complex-membered ext-real-membered real-membered non left_end interval set
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
].x,c₇.] is ext-real-membered non left_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is V24() real ext-real Element of REAL
eps1 * x is V24() real ext-real Element of REAL
c₉ is ext-real Element of ExtREAL
].c₇,c₉.] is ext-real-membered non left_end interval set
q is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
2r is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
q is set
z2 is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
1ra is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is ext-real Element of ExtREAL
d is V24() real ext-real set
].eps1,d.] is complex-membered ext-real-membered real-membered non left_end interval set
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
[.c₇,x.[ is ext-real-membered non right_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
eps1 * z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
x is ext-real Element of ExtREAL
c₇ is V24() real ext-real Element of REAL
eps1 * c₇ is V24() real ext-real Element of REAL
c₉ is ext-real Element of ExtREAL
[.c₉,x.[ is ext-real-membered non right_end interval set
q is set
z2 is V24() real ext-real Element of REAL
z2 / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(z2,K107(eps1)) is V24() real ext-real set
z2 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r is ext-real Element of ExtREAL
2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
2r1 / eps1 is V24() real ext-real Element of REAL
K105(2r1,K107(eps1)) is V24() real ext-real set
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
eps1 * z2 is V24() real ext-real Element of REAL
eps1 * (z2 / eps1) is V24() real ext-real Element of REAL
q is set
z2 is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
1ra is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
r1 is ext-real Element of ExtREAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
[.(inf eps),(sup eps).] is ext-real-membered interval set
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps1 is ext-real Element of ExtREAL
sup eps1 is ext-real Element of ExtREAL
[.(inf eps1),(sup eps1).] is ext-real-membered interval set
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
r2 is ext-real Element of ExtREAL
c₇ is ext-real Element of ExtREAL
[.r2,c₇.] is ext-real-membered interval set
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
2o / eps1 is V24() real ext-real Element of REAL
K105(2o,K107(eps1)) is V24() real ext-real set
2r / eps1 is V24() real ext-real Element of REAL
K105(2r,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is V24() real ext-real Element of REAL
2o is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1o is ext-real Element of ExtREAL
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
].(inf eps),(sup eps).] is ext-real-membered non left_end interval set
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps1 is ext-real Element of ExtREAL
sup eps1 is ext-real Element of ExtREAL
].(inf eps1),(sup eps1).] is ext-real-membered non left_end interval set
r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
].c₇,x.] is ext-real-membered non left_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
2o is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
2r / eps1 is V24() real ext-real Element of REAL
K105(2r,K107(eps1)) is V24() real ext-real set
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
2o is ext-real Element of ExtREAL
2r1 is V24() real ext-real Element of REAL
1o is V24() real ext-real Element of REAL
eps1 * 2r1 is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
d is V24() real ext-real set
].(inf eps),d.] is complex-membered ext-real-membered real-membered non left_end interval set
r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
].(inf eps),(sup eps).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps1 is ext-real Element of ExtREAL
sup eps1 is ext-real Element of ExtREAL
].(inf eps1),(sup eps1).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
r2 is ext-real Element of ExtREAL
c₇ is ext-real Element of ExtREAL
].r2,c₇.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)
x is set
c₉ is V24() real ext-real Element of REAL
c₉ / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(c₉,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
2r / eps1 is V24() real ext-real Element of REAL
K105(2r,K107(eps1)) is V24() real ext-real set
2o / eps1 is V24() real ext-real Element of REAL
K105(2o,K107(eps1)) is V24() real ext-real set
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
eps1 * (c₉ / eps1) is V24() real ext-real Element of REAL
x is set
c₉ is V24() real ext-real Element of REAL
q is V24() real ext-real Element of REAL
eps1 * q is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
z2 is V24() real ext-real Element of REAL
2o is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
eps1 * 2o1 is V24() real ext-real Element of REAL
2r1 is ext-real Element of ExtREAL
1o is ext-real Element of ExtREAL
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 * d is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
[.(inf eps),(sup eps).[ is ext-real-membered non right_end interval set
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
inf eps1 is ext-real Element of ExtREAL
sup eps1 is ext-real Element of ExtREAL
[.(inf eps1),(sup eps1).[ is ext-real-membered non right_end interval set
r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
c₇ is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
[.c₇,x.[ is ext-real-membered non right_end interval set
c₉ is set
q is V24() real ext-real Element of REAL
q / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(q,K107(eps1)) is V24() real ext-real set
z2 is ext-real Element of ExtREAL
2o is ext-real Element of ExtREAL
2r is V24() real ext-real Element of REAL
2o1 is V24() real ext-real Element of REAL
2o1 / eps1 is V24() real ext-real Element of REAL
K105(2o1,K107(eps1)) is V24() real ext-real set
2r / eps1 is V24() real ext-real Element of REAL
K105(2r,K107(eps1)) is V24() real ext-real set
eps1 * (q / eps1) is V24() real ext-real Element of REAL
eps1 * (q / eps1) is V24() real ext-real Element of REAL
c₉ is set
q is V24() real ext-real Element of REAL
z2 is V24() real ext-real Element of REAL
eps1 * z2 is V24() real ext-real Element of REAL
z2 is ext-real Element of ExtREAL
2o is V24() real ext-real Element of REAL
2r is V24() real ext-real Element of REAL
eps1 * 2o is V24() real ext-real Element of REAL
eps1 * 2r is V24() real ext-real Element of REAL
2o1 is ext-real Element of ExtREAL
2r1 is ext-real Element of ExtREAL
1o is V24() real ext-real Element of REAL
1ra is V24() real ext-real Element of REAL
eps1 * 1o is V24() real ext-real Element of REAL
eps1 * 1ra is V24() real ext-real Element of REAL
d is V24() real ext-real set
[.d,(sup eps).[ is complex-membered ext-real-membered real-membered non right_end interval set
r1 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is ext-real-membered set
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
sup (eps1 ** eps) is ext-real Element of ExtREAL
eps1 is V24() real ext-real set
eps1 * eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
d / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(d,K107(eps1)) is V24() real ext-real set
r1 is ext-real set
eps1 " is V24() real ext-real Element of REAL
(eps1 ") ** (eps1 ** eps) is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{(eps1 ")} is non empty complex-membered ext-real-membered real-membered set
{(eps1 ")} ** (eps1 ** eps) is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
{(eps1 ")} ** (eps1 ** eps) is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
(eps1 ") ** (eps1 ** eps) is non empty ext-real-membered set
r2 is V24() real ext-real Element of REAL
(eps1 ") * r2 is V24() real ext-real Element of REAL
r2 / eps1 is V24() real ext-real Element of REAL
K105(r2,K107(eps1)) is V24() real ext-real set
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
sup eps is ext-real Element of ExtREAL
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
sup (eps1 ** eps) is ext-real Element of ExtREAL
eps1 is ext-real Element of ExtREAL
eps1 * (sup eps) is ext-real Element of ExtREAL
d is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 * +infty is ext-real Element of ExtREAL
r1 is non empty complex-membered ext-real-membered real-membered bounded_above set
upper_bound r1 is V24() real ext-real set
sup r1 is V24() real ext-real set
eps1 ** r1 is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} ** r1 is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in r1 ) } is set
{eps1} ** r1 is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in r1 ) } is set
eps1 ** r1 is non empty ext-real-membered set
d is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
c₇ is non empty complex-membered ext-real-membered real-membered bounded_above set
upper_bound c₇ is V24() real ext-real set
sup c₇ is V24() real ext-real set
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
inf (eps1 ** eps) is ext-real Element of ExtREAL
eps1 is V24() real ext-real set
eps1 * eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
d / eps1 is V24() real ext-real Element of REAL
K107(eps1) is V24() real ext-real set
K105(d,K107(eps1)) is V24() real ext-real set
r1 is ext-real set
eps1 " is V24() real ext-real Element of REAL
(eps1 ") ** (eps1 ** eps) is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{(eps1 ")} is non empty complex-membered ext-real-membered real-membered set
{(eps1 ")} ** (eps1 ** eps) is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
{(eps1 ")} ** (eps1 ** eps) is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {(eps1 ")} & b₂ in eps1 ** eps ) } is set
(eps1 ") ** (eps1 ** eps) is non empty ext-real-membered set
r2 is V24() real ext-real Element of REAL
(eps1 ") * r2 is V24() real ext-real Element of REAL
r2 / eps1 is V24() real ext-real Element of REAL
K105(r2,K107(eps1)) is V24() real ext-real set
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
inf eps is ext-real Element of ExtREAL
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
inf (eps1 ** eps) is ext-real Element of ExtREAL
eps1 is ext-real Element of ExtREAL
eps1 * (inf eps) is ext-real Element of ExtREAL
d is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 * -infty is ext-real Element of ExtREAL
r1 is non empty complex-membered ext-real-membered real-membered bounded_below set
lower_bound r1 is V24() real ext-real set
inf r1 is V24() real ext-real set
eps1 ** r1 is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} ** r1 is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in r1 ) } is set
{eps1} ** r1 is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in r1 ) } is set
eps1 ** r1 is non empty ext-real-membered set
d is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
c₇ is non empty complex-membered ext-real-membered real-membered bounded_below set
lower_bound c₇ is V24() real ext-real set
inf c₇ is V24() real ext-real set
r2 is V24() real ext-real Element of REAL
eps1 * r2 is V24() real ext-real Element of REAL
eps is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
diameter eps is ext-real Element of ExtREAL
eps1 is V24() real ext-real Element of REAL
eps1 ** eps is complex-membered ext-real-membered real-membered interval Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is ext-real-membered set
diameter (eps1 ** eps) is ext-real Element of ExtREAL
eps1 is V24() real ext-real Element of REAL
eps1 * eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real set
r1 is V24() real ext-real Element of REAL
eps1 * r1 is V24() real ext-real Element of REAL
r2 is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 ** r2 is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} ** r2 is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in r2 ) } is set
{eps1} ** r2 is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in r2 ) } is set
eps1 ** r2 is non empty ext-real-membered set
inf (eps1 ** r2) is ext-real Element of ExtREAL
c₇ is ext-real Element of ExtREAL
inf r2 is ext-real Element of ExtREAL
c₇ * (inf r2) is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
x * (diameter eps) is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
inf eps is ext-real Element of ExtREAL
(sup eps) - (inf eps) is ext-real Element of ExtREAL
x * ((sup eps) - (inf eps)) is ext-real Element of ExtREAL
x * (sup eps) is ext-real Element of ExtREAL
x * (inf eps) is ext-real Element of ExtREAL
(x * (sup eps)) - (x * (inf eps)) is ext-real Element of ExtREAL
sup (eps1 ** eps) is ext-real Element of ExtREAL
inf (eps1 ** eps) is ext-real Element of ExtREAL
(sup (eps1 ** eps)) - (inf (eps1 ** eps)) is ext-real Element of ExtREAL
eps is V24() real ext-real Element of REAL
1 / eps is V24() real ext-real Element of REAL
K107(eps) is V24() real ext-real set
K105(1,K107(eps)) is V24() real ext-real set
eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
2 |^ eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
(2 |^ eps1) * eps is V24() real ext-real Element of REAL
(1 / eps) * eps is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
eps1 - eps is V24() real ext-real Element of REAL
K106(eps) is V24() real ext-real set
K104(eps1,K106(eps)) is V24() real ext-real set
[\eps/] is V24() real ext-real integer set
[\eps/] + 1 is V24() real ext-real integer Element of REAL
eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
eps + 1 is V24() real ext-real Element of REAL
1 + eps is V24() real ext-real Element of REAL
eps is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is set
eps1 is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps1 - eps is V24() real ext-real Element of REAL
K106(eps) is V24() real ext-real set
K104(eps1,K106(eps)) is V24() real ext-real set
d is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
2 |^ d is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
(2 |^ d) * (eps1 - eps) is V24() real ext-real Element of REAL
(2 |^ d) * eps is V24() real ext-real Element of REAL
(2 |^ d) * eps1 is V24() real ext-real Element of REAL
((2 |^ d) * eps1) - ((2 |^ d) * eps) is V24() real ext-real Element of REAL
K106(((2 |^ d) * eps)) is V24() real ext-real set
K104(((2 |^ d) * eps1),K106(((2 |^ d) * eps))) is V24() real ext-real set
c₇ is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
c₇ / (2 |^ d) is V24() real ext-real non negative Element of REAL
K107((2 |^ d)) is V24() real ext-real non negative set
K105(c₇,K107((2 |^ d))) is V24() real ext-real non negative set
dyadic d is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps1 is V24() real ext-real set
{ b₁ where b₁ is V24() real ext-real Element of REAL : not 0 <= b₁ } is set
d is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
eps1 is V24() real ext-real set
{ b₁ where b₁ is V24() real ext-real Element of REAL : not b₁ <= 1 } is set
d is V24() real ext-real Element of REAL
DYADIC \/ (right_open_halfline 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
(halfline 0) \/ (DYADIC \/ (right_open_halfline 1)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
d is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
eps is non empty ext-real-membered Element of K32(ExtREAL)
inf eps is ext-real Element of ExtREAL
sup eps is ext-real Element of ExtREAL
eps1 is ext-real Element of ExtREAL
eps1 is ext-real Element of ExtREAL
[.eps1,eps1.] is ext-real-membered interval set
d is non empty ext-real-membered Element of K32(ExtREAL)
r1 is ext-real set
r1 is ext-real set
dyadic 0 is complex-membered ext-real-membered real-membered Element of K32(REAL)
[.0,1.] is complex-membered ext-real-membered real-membered interval set
eps is set
eps1 is V24() real ext-real Element of REAL
eps1 is ext-real Element of ExtREAL
d is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic d is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic eps is complex-membered ext-real-membered real-membered Element of K32(REAL)
dyadic eps1 is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
eps + eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic (eps + eps1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 + 1 is non empty ordinal natural V24() real ext-real positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V134() Element of NAT
eps + (eps1 + 1) is non empty ordinal natural V24() real ext-real positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V134() Element of NAT
dyadic (eps + (eps1 + 1)) is complex-membered ext-real-membered real-membered Element of K32(REAL)
(eps + eps1) + 1 is non empty ordinal natural V24() real ext-real positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V134() Element of NAT
dyadic ((eps + eps1) + 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps + 0 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic (eps + 0) is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
eps + eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
dyadic (eps + eps1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 is ordinal natural V24() real ext-real non negative integer set
eps + eps1 is ordinal natural V24() real ext-real non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V134() Element of NAT
eps1 is V24() real ext-real Element of REAL
eps is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
d is V24() real ext-real Element of REAL
eps1 - eps is V24() real ext-real Element of REAL
K106(eps) is V24() real ext-real set
K104(eps1,K106(eps)) is V24() real ext-real set
d - eps1 is V24() real ext-real Element of REAL
K106(eps1) is V24() real ext-real set
K104(d,K106(eps1)) is V24() real ext-real set
abs (d - eps1) is V24() real ext-real Element of REAL
eps1 + d is V24() real ext-real Element of REAL
eps1 + eps is V24() real ext-real Element of REAL
eps1 - d is V24() real ext-real Element of REAL
K106(d) is V24() real ext-real set
K104(eps1,K106(d)) is V24() real ext-real set
- (eps1 - eps) is V24() real ext-real Element of REAL
- (eps1 - d) is V24() real ext-real Element of REAL
eps1 + eps1 is V24() real ext-real Element of REAL
eps + d is V24() real ext-real Element of REAL
- (d - eps1) is V24() real ext-real Element of REAL
DYADIC \/ (right_open_halfline 1) is complex-membered ext-real-membered real-membered Element of K32(REAL)
eps is V24() real ext-real Element of REAL
eps1 is V24() real ext-real set
d is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
d - eps1 is V24() real ext-real Element of REAL
K106(eps1) is V24() real ext-real set
K104(d,K106(eps1)) is V24() real ext-real set
d - 0 is V24() real ext-real Element of REAL
K106(0) is empty V24() real ext-real non positive non negative integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set
K104(d,K106(0)) is V24() real ext-real set
r1 is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
eps - eps1 is V24() real ext-real Element of REAL
K104(eps,K106(eps1)) is V24() real ext-real set
eps - eps is V24() real ext-real Element of REAL
K106(eps) is V24() real ext-real set
K104(eps,K106(eps)) is V24() real ext-real set
d + (eps - eps1) is V24() real ext-real Element of REAL
d + 0 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
r2 - r1 is V24() real ext-real Element of REAL
K106(r1) is V24() real ext-real set
K104(r2,K106(r1)) is V24() real ext-real set
(d + (eps - eps1)) - (d - eps1) is V24() real ext-real Element of REAL
K106((d - eps1)) is V24() real ext-real set
K104((d + (eps - eps1)),K106((d - eps1))) is V24() real ext-real set
abs (r2 - r1) is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
r1 is V24() real ext-real Element of REAL
r1 + eps1 is V24() real ext-real Element of REAL
0 + d is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
r2 is V24() real ext-real Element of REAL
r2 - r1 is V24() real ext-real Element of REAL
K106(r1) is V24() real ext-real set
K104(r2,K106(r1)) is V24() real ext-real set
(r1 + eps1) - r1 is V24() real ext-real Element of REAL
K104((r1 + eps1),K106(r1)) is V24() real ext-real set
eps1 is V24() real ext-real Element of REAL
eps1 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set
eps1 is V24() real ext-real Element of REAL
eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
eps1 ** eps is non empty complex-membered ext-real-membered real-membered Element of K32(REAL)
{eps1} is non empty complex-membered ext-real-membered real-membered set
{eps1} ** eps is non empty complex-membered ext-real-membered real-membered set
{ K573(b₁,b₂) where b₁, b₂ is V24() Element of COMPLEX : ( b₁ in {eps1} & b₂ in eps ) } is set
{eps1} ** eps is non empty ext-real-membered set
{ (b₁ * b₂) where b₁, b₂ is ext-real Element of ExtREAL : ( b₁ in {eps1} & b₂ in eps ) } is set
eps1 ** eps is non empty ext-real-membered set