:: 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

{eps1} ** eps is ext-real-membered set

{ (b

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

{(eps1 ")} ** (eps1 ** eps) is ext-real-membered set

{ (b

(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

{eps} ** eps1 is ext-real-membered set

{ (b

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

{0} ** eps is ext-real-membered set

{ (b

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

{eps} ** {} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V72() bounded_below interval set

{ (b

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

{0} ** eps is ext-real-membered set

{ (b

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

].c

x is set

c

c

K107(eps1) is V24() real ext-real set

K105(c

z2 is ext-real Element of ExtREAL

eps1 * (c

z2 is ext-real Element of ExtREAL

eps1 * (c

x is set

c

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

].x,c

c

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

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

].-infty,c

x is set

c

c

K107(eps1) is V24() real ext-real set

K105(c

eps1 * (c

z2 is ext-real Element of ExtREAL

z2 is ext-real Element of ExtREAL

x is set

c

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

].-infty,c

x is set

c

c

K107(eps1) is V24() real ext-real set

K105(c

z2 is ext-real Element of ExtREAL

eps1 * (c

z2 is ext-real Element of ExtREAL

eps1 * (c

x is set

c

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

x is ext-real Element of ExtREAL

].c

c

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

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

].c

x is set

c

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

c

K107(eps1) is V24() real ext-real set

K105(c

eps1 * (c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

eps1 * c

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

[.q,c

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

eps1 * c

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

[.q,c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is V24() real ext-real Element of REAL

eps1 * x is V24() real ext-real Element of REAL

c

[.c

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

x is ext-real Element of ExtREAL

[.c

c

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

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is V24() real ext-real Element of REAL

eps1 * x is V24() real ext-real Element of REAL

c

].c

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

x is ext-real Element of ExtREAL

].x,c

c

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

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is ext-real Element of ExtREAL

].x,c

c

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

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

x is V24() real ext-real Element of REAL

eps1 * x is V24() real ext-real Element of REAL

c

].c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is ext-real Element of ExtREAL

[.c

c

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

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

eps1 * c

c

[.c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

[.r2,c

x is set

c

c

K107(eps1) is V24() real ext-real set

K105(c

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 * (c

x is set

c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is ext-real Element of ExtREAL

].c

c

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

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

].r2,c

x is set

c

c

K107(eps1) is V24() real ext-real set

K105(c

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 * (c

x is set

c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

x is ext-real Element of ExtREAL

[.c

c

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

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

{eps1} ** eps is ext-real-membered set

{ (b

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

{(eps1 ")} ** (eps1 ** eps) is non empty ext-real-membered set

{ (b

(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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

{eps1} ** r1 is non empty ext-real-membered set

{ (b

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

upper_bound c

sup c

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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

{(eps1 ")} ** (eps1 ** eps) is non empty ext-real-membered set

{ (b

(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

{eps1} ** eps is non empty ext-real-membered set

{ (b

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

{eps1} ** r1 is non empty ext-real-membered set

{ (b

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

lower_bound c

inf c

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

{eps1} ** eps is ext-real-membered set

{ (b

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

{eps1} ** r2 is non empty ext-real-membered set

{ (b

eps1 ** r2 is non empty ext-real-membered set

inf (eps1 ** r2) is ext-real Element of ExtREAL

c

inf r2 is ext-real Element of ExtREAL

c

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

c

K107((2 |^ d)) is V24() real ext-real non negative set

K105(c

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

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

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