:: TOPS_4 semantic presentation

NAT is V134() V135() V136() V137() V138() V139() V140() Element of K6(REAL)

REAL is V134() V135() V136() V140() set

K6(REAL) is set

omega is V134() V135() V136() V137() V138() V139() V140() set

K6(omega) is set

K6(NAT) is set

INT is V134() V135() V136() V137() V138() V140() set

1 is set

K7(1,1) is V16() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V16() set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is V16() V124() V125() V126() set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is V16() V124() V125() V126() set

K7(K7(REAL,REAL),REAL) is V16() V124() V125() V126() set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is set

K7(2,2) is V16() set

K7(K7(2,2),REAL) is V16() V124() V125() V126() set

K6(K7(K7(2,2),REAL)) is set

COMPLEX is V134() V140() set

RAT is V134() V135() V136() V137() V140() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is V158() L15()

the U1 of (TOP-REAL 2) is set

K405() is V189() TopStruct

the U1 of K405() is V134() V135() V136() set

RealSpace is non empty strict Reflexive discerning V83() triangle Discerning V189() MetrStruct

real_dist is V16() Function-like V30(K7(REAL,REAL), REAL ) V124() V125() V126() Element of K6(K7(K7(REAL,REAL),REAL))

MetrStruct(# REAL,real_dist #) is strict MetrStruct

R^1 is non empty strict TopSpace-like V189() TopStruct

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

the U1 of RealSpace is V1() V134() V135() V136() set

Family_open_set RealSpace is Element of K6(K6( the U1 of RealSpace))

K6( the U1 of RealSpace) is set

K6(K6( the U1 of RealSpace)) is set

TopStruct(# the U1 of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct

K412() is TopSpace-like V189() SubSpace of R^1

K390(K412(),K412()) is strict TopSpace-like TopStruct

the U1 of K390(K412(),K412()) is set

K414() is non empty strict TopSpace-like V189() V191() SubSpace of R^1

the U1 of K414() is V1() V134() V135() V136() set

K6( the U1 of K414()) is set

K6(K6( the U1 of K414())) is set

K423(2) is TopSpace-like V192() SubSpace of TOP-REAL 2

the U1 of K423(2) is set

K7( the U1 of K414(), the U1 of K423(2)) is V16() set

K6(K7( the U1 of K414(), the U1 of K423(2))) is set

K427() is V16() Function-like V30( the U1 of K414(), the U1 of K423(2)) V30( the U1 of K414(), the U1 of K423(2)) V31( the U1 of K423(2)) continuous Element of K6(K7( the U1 of K414(), the U1 of K423(2)))

K424() is Element of the U1 of K423(2)

0 is V1() natural V11() real ext-real non positive non negative V16() non-empty empty-yielding V20( RAT ) V33() V34() V124() V125() V126() V127() V134() V135() V136() V137() V138() V139() V140() Element of NAT

|[1,0]| is Element of the U1 of (TOP-REAL 2)

K426(K424()) is non empty strict TopSpace-like SubSpace of K423(2)

the U1 of K426(K424()) is V1() set

].0,1.[ is V1() V134() V135() V136() Element of K6(REAL)

R^1 ].0,1.[ is V1() V134() V135() V136() Element of K6( the U1 of K414())

K414() | (R^1 ].0,1.[) is non empty strict TopSpace-like V189() SubSpace of K414()

the U1 of (K414() | (R^1 ].0,1.[)) is V1() V134() V135() V136() set

K7( the U1 of K426(K424()), the U1 of (K414() | (R^1 ].0,1.[))) is V16() V124() V125() V126() set

K6(K7( the U1 of K426(K424()), the U1 of (K414() | (R^1 ].0,1.[)))) is set

K425() is Element of the U1 of K423(2)

K313(1) is V11() real ext-real Element of REAL

|[K313(1),0]| is Element of the U1 of (TOP-REAL 2)

K426(K425()) is non empty strict TopSpace-like SubSpace of K423(2)

the U1 of K426(K425()) is V1() set

K322(1,2) is V11() real ext-real Element of REAL

3 is set

K322(3,2) is V11() real ext-real Element of REAL

].K322(1,2),K322(3,2).[ is V1() V134() V135() V136() open Element of K6(REAL)

R^1 ].K322(1,2),K322(3,2).[ is V1() open V134() V135() V136() Element of K6( the U1 of K414())

K414() | (R^1 ].K322(1,2),K322(3,2).[) is non empty strict TopSpace-like V189() SubSpace of K414()

the U1 of (K414() | (R^1 ].K322(1,2),K322(3,2).[)) is V1() V134() V135() V136() set

K7( the U1 of K426(K425()), the U1 of (K414() | (R^1 ].K322(1,2),K322(3,2).[))) is V16() V124() V125() V126() set

K6(K7( the U1 of K426(K425()), the U1 of (K414() | (R^1 ].K322(1,2),K322(3,2).[)))) is set

0 is V1() V16() non-empty empty-yielding V20( RAT ) V124() V125() V126() V127() V134() V135() V136() V137() V138() V139() V140() set

the U1 of R^1 is V1() V134() V135() V136() set

K6( the U1 of R^1) is set

m is TopSpace-like TopStruct

the U1 of m is set

f1 is TopSpace-like TopStruct

the U1 of f1 is set

K7( the U1 of m, the U1 of f1) is V16() set

K6(K7( the U1 of m, the U1 of f1)) is set

f is TopSpace-like TopStruct

the U1 of f is set

p is TopSpace-like TopStruct

the U1 of p is set

K7( the U1 of f, the U1 of p) is V16() set

K6(K7( the U1 of f, the U1 of p)) is set

the topology of m is V1() Element of K6(K6( the U1 of m))

K6( the U1 of m) is set

K6(K6( the U1 of m)) is set

TopStruct(# the U1 of m, the topology of m #) is strict TopSpace-like TopStruct

the topology of f is V1() Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f, the topology of f #) is strict TopSpace-like TopStruct

the topology of f1 is V1() Element of K6(K6( the U1 of f1))

K6( the U1 of f1) is set

K6(K6( the U1 of f1)) is set

TopStruct(# the U1 of f1, the topology of f1 #) is strict TopSpace-like TopStruct

the topology of p is V1() Element of K6(K6( the U1 of p))

K6( the U1 of p) is set

K6(K6( the U1 of p)) is set

TopStruct(# the U1 of p, the topology of p #) is strict TopSpace-like TopStruct

q is V16() Function-like V30( the U1 of m, the U1 of f1) Element of K6(K7( the U1 of m, the U1 of f1))

r is V16() Function-like V30( the U1 of f, the U1 of p) Element of K6(K7( the U1 of f, the U1 of p))

p1 is Element of K6( the U1 of f)

r .: p1 is Element of K6( the U1 of p)

s is Element of K6( the U1 of m)

q .: s is Element of K6( the U1 of f1)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

K6( the U1 of (TOP-REAL m)) is set

f is Element of K6( the U1 of (TOP-REAL m))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

q is Element of the U1 of (Euclid m)

r is V11() real ext-real set

Ball (q,r) is Element of K6( the U1 of (Euclid m))

p1 is V1() V11() real ext-real positive non negative set

s is V1() V11() real ext-real positive non negative set

Ball (p,s) is V1() open Element of K6( the U1 of (TOP-REAL m))

p is Element of the U1 of (Euclid m)

q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V1() open Element of K6( the U1 of (TOP-REAL m))

Ball (p,r) is Element of K6( the U1 of (Euclid m))

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

f is non empty TopSpace-like TopStruct

the U1 of f is V1() set

K7( the U1 of m, the U1 of f) is V16() set

K6(K7( the U1 of m, the U1 of f)) is set

K6( the U1 of m) is set

K6( the U1 of f) is set

f1 is V16() Function-like V30( the U1 of m, the U1 of f) Element of K6(K7( the U1 of m, the U1 of f))

p is Element of the U1 of m

f1 . p is Element of the U1 of f

q is open Element of K6( the U1 of m)

f1 .: q is Element of K6( the U1 of f)

r is V1() open a_neighborhood of f1 . p

p is Element of the U1 of m

f1 . p is Element of the U1 of f

q is V1() open a_neighborhood of p

f1 .: q is Element of K6( the U1 of f)

r is open Element of K6( the U1 of f)

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K6( the U1 of m) is set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of m, the U1 of (TopSpaceMetr f)) is V16() set

K6(K7( the U1 of m, the U1 of (TopSpaceMetr f))) is set

f1 is V16() Function-like V30( the U1 of m, the U1 of (TopSpaceMetr f)) Element of K6(K7( the U1 of m, the U1 of (TopSpaceMetr f)))

p is Element of the U1 of m

f1 . p is Element of the U1 of (TopSpaceMetr f)

q is open Element of K6( the U1 of m)

f1 .: q is Element of K6( the U1 of (TopSpaceMetr f))

K6( the U1 of (TopSpaceMetr f)) is set

r is Element of the U1 of f

p1 is open Element of K6( the U1 of (TopSpaceMetr f))

s is V11() real ext-real set

Ball (r,s) is Element of K6( the U1 of f)

K6( the U1 of (TopSpaceMetr f)) is set

p is Element of the U1 of m

f1 . p is Element of the U1 of (TopSpaceMetr f)

q is open Element of K6( the U1 of m)

f1 .: q is Element of K6( the U1 of (TopSpaceMetr f))

r is Element of the U1 of f

p1 is V1() V11() real ext-real positive non negative set

Ball (r,p1) is Element of K6( the U1 of f)

s is open Element of K6( the U1 of (TopSpaceMetr f))

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K6( the U1 of m) is set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of (TopSpaceMetr f), the U1 of m) is V16() set

K6(K7( the U1 of (TopSpaceMetr f), the U1 of m)) is set

f1 is V16() Function-like V30( the U1 of (TopSpaceMetr f), the U1 of m) Element of K6(K7( the U1 of (TopSpaceMetr f), the U1 of m))

p is Element of the U1 of f

q is V1() V11() real ext-real positive non negative set

Ball (p,q) is Element of K6( the U1 of f)

K6( the U1 of (TopSpaceMetr f)) is set

r is Element of K6( the U1 of (TopSpaceMetr f))

f1 . p is set

f1 .: r is Element of K6( the U1 of m)

p1 is open Element of K6( the U1 of m)

s is open Element of K6( the U1 of m)

f1 .: (Ball (p,q)) is Element of K6( the U1 of m)

p is Element of the U1 of (TopSpaceMetr f)

f1 . p is Element of the U1 of m

q is open Element of K6( the U1 of (TopSpaceMetr f))

f1 .: q is Element of K6( the U1 of m)

r is Element of the U1 of f

p1 is V11() real ext-real set

Ball (r,p1) is Element of K6( the U1 of f)

f1 .: (Ball (r,p1)) is Element of K6( the U1 of m)

s is open Element of K6( the U1 of m)

m is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr m is non empty strict TopSpace-like TopStruct

the U1 of m is V1() set

Family_open_set m is Element of K6(K6( the U1 of m))

K6( the U1 of m) is set

K6(K6( the U1 of m)) is set

TopStruct(# the U1 of m,(Family_open_set m) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr m) is V1() set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)) is V16() set

K6(K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f))) is set

f1 is V16() Function-like V30( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)) Element of K6(K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)))

p is Element of the U1 of m

f1 . p is set

q is Element of the U1 of f

r is V1() V11() real ext-real positive non negative set

Ball (p,r) is Element of K6( the U1 of m)

f1 .: (Ball (p,r)) is Element of K6( the U1 of (TopSpaceMetr f))

K6( the U1 of (TopSpaceMetr f)) is set

K6( the U1 of (TopSpaceMetr m)) is set

p1 is Element of K6( the U1 of (TopSpaceMetr m))

K6( the U1 of (TopSpaceMetr m)) is set

p is Element of the U1 of (TopSpaceMetr m)

f1 . p is Element of the U1 of (TopSpaceMetr f)

q is open Element of K6( the U1 of (TopSpaceMetr m))

f1 .: q is Element of K6( the U1 of (TopSpaceMetr f))

K6( the U1 of (TopSpaceMetr f)) is set

r is Element of the U1 of f

p1 is Element of the U1 of m

s is V11() real ext-real set

Ball (p1,s) is Element of K6( the U1 of m)

f1 .: (Ball (p1,s)) is Element of K6( the U1 of (TopSpaceMetr f))

c

Ball (r,c

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is non empty TopSpace-like TopStruct

the U1 of f is V1() set

K7( the U1 of f, the U1 of (TOP-REAL m)) is V16() set

K6(K7( the U1 of f, the U1 of (TOP-REAL m))) is set

K6( the U1 of f) is set

f1 is V16() Function-like V30( the U1 of f, the U1 of (TOP-REAL m)) Element of K6(K7( the U1 of f, the U1 of (TOP-REAL m)))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K7( the U1 of f, the U1 of (TopSpaceMetr (Euclid m))) is V16() set

K6(K7( the U1 of f, the U1 of (TopSpaceMetr (Euclid m)))) is set

the topology of f is V1() Element of K6(K6( the U1 of f))

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f, the topology of f #) is non empty strict TopSpace-like TopStruct

q is Element of the U1 of f

f1 . q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

r is open Element of K6( the U1 of f)

f1 .: r is Element of K6( the U1 of (TOP-REAL m))

p is V16() Function-like V30( the U1 of f, the U1 of (TopSpaceMetr (Euclid m))) Element of K6(K7( the U1 of f, the U1 of (TopSpaceMetr (Euclid m))))

p1 is Element of the U1 of (Euclid m)

p .: r is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

s is V1() V11() real ext-real positive non negative set

Ball (p1,s) is Element of K6( the U1 of (Euclid m))

Ball ((f1 . q),s) is V1() open Element of K6( the U1 of (TOP-REAL m))

p is V16() Function-like V30( the U1 of f, the U1 of (TopSpaceMetr (Euclid m))) Element of K6(K7( the U1 of f, the U1 of (TopSpaceMetr (Euclid m))))

q is Element of the U1 of f

p . q is Element of the U1 of (TopSpaceMetr (Euclid m))

r is open Element of K6( the U1 of f)

p .: r is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

p1 is Element of the U1 of (Euclid m)

f1 . q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 .: r is Element of K6( the U1 of (TOP-REAL m))

s is V1() V11() real ext-real positive non negative set

Ball ((f1 . q),s) is V1() open Element of K6( the U1 of (TOP-REAL m))

Ball (p1,s) is Element of K6( the U1 of (Euclid m))

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is non empty TopSpace-like TopStruct

the U1 of f is V1() set

K7( the U1 of (TOP-REAL m), the U1 of f) is V16() set

K6(K7( the U1 of (TOP-REAL m), the U1 of f)) is set

K6( the U1 of f) is set

f1 is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of f) Element of K6(K7( the U1 of (TOP-REAL m), the U1 of f))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f) is V16() set

K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f)) is set

the topology of f is V1() Element of K6(K6( the U1 of f))

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f, the topology of f #) is non empty strict TopSpace-like TopStruct

q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . q is Element of the U1 of f

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: (Ball (q,r)) is Element of K6( the U1 of f)

p is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f) Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f))

p . q is set

p1 is Element of the U1 of (Euclid m)

Ball (p1,r) is Element of K6( the U1 of (Euclid m))

p .: (Ball (p1,r)) is Element of K6( the U1 of f)

s is open Element of K6( the U1 of f)

p is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f) Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of f))

q is Element of the U1 of (Euclid m)

p . q is set

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is Element of K6( the U1 of (Euclid m))

p .: (Ball (q,r)) is Element of K6( the U1 of f)

p1 is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . p1 is Element of the U1 of f

Ball (p1,r) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: (Ball (p1,r)) is Element of K6( the U1 of f)

s is open Element of K6( the U1 of f)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is natural V11() real ext-real set

TOP-REAL f is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL f) is V1() set

K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)) is V16() set

K6(K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f))) is set

f1 is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)) Element of K6(K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the topology of (TOP-REAL f) is V1() Element of K6(K6( the U1 of (TOP-REAL f)))

K6( the U1 of (TOP-REAL f)) is set

K6(K6( the U1 of (TOP-REAL f))) is set

TopStruct(# the U1 of (TOP-REAL f), the topology of (TOP-REAL f) #) is non empty strict TopSpace-like TopStruct

Euclid f is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid f) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid f) is V1() set

Family_open_set (Euclid f) is Element of K6(K6( the U1 of (Euclid f)))

K6( the U1 of (Euclid f)) is set

K6(K6( the U1 of (Euclid f))) is set

TopStruct(# the U1 of (Euclid f),(Family_open_set (Euclid f)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

the U1 of (TopSpaceMetr (Euclid f)) is V1() set

K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))) is V16() set

K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f)))) is set

q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . q is V42(f) V43() V126() Element of the U1 of (TOP-REAL f)

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: (Ball (q,r)) is Element of K6( the U1 of (TOP-REAL f))

p is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))) Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))))

s is Element of the U1 of (Euclid f)

p1 is Element of the U1 of (Euclid m)

Ball (p1,r) is Element of K6( the U1 of (Euclid m))

p .: (Ball (p1,r)) is Element of K6( the U1 of (TopSpaceMetr (Euclid f)))

K6( the U1 of (TopSpaceMetr (Euclid f))) is set

c

Ball (s,c

Ball ((f1 . q),c

p is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))) Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))))

q is Element of the U1 of (Euclid m)

p . q is set

r is Element of the U1 of (Euclid f)

p1 is V1() V11() real ext-real positive non negative set

Ball (q,p1) is Element of K6( the U1 of (Euclid m))

p .: (Ball (q,p1)) is Element of K6( the U1 of (TopSpaceMetr (Euclid f)))

K6( the U1 of (TopSpaceMetr (Euclid f))) is set

c

s is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

Ball (s,p1) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: (Ball (s,p1)) is Element of K6( the U1 of (TOP-REAL f))

c

Ball (c

Ball (r,c

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K7( the U1 of m, the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of m, the U1 of R^1)) is set

K6( the U1 of m) is set

f is V16() Function-like V30( the U1 of m, the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of m, the U1 of R^1))

f1 is Element of the U1 of m

f . f1 is V11() real ext-real Element of the U1 of R^1

p is open Element of K6( the U1 of m)

f .: p is V134() V135() V136() Element of K6( the U1 of R^1)

q is V11() real ext-real Element of the U1 of RealSpace

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

q - r is V11() real ext-real set

q + r is V11() real ext-real set

].(q - r),(q + r).[ is V134() V135() V136() open Element of K6(REAL)

f1 is Element of the U1 of m

f . f1 is V11() real ext-real Element of the U1 of R^1

p is open Element of K6( the U1 of m)

f .: p is V134() V135() V136() Element of K6( the U1 of R^1)

q is V11() real ext-real Element of the U1 of RealSpace

r is V1() V11() real ext-real positive non negative set

(f . f1) - r is V11() real ext-real set

(f . f1) + r is V11() real ext-real set

].((f . f1) - r),((f . f1) + r).[ is V134() V135() V136() open Element of K6(REAL)

q - r is V11() real ext-real set

q + r is V11() real ext-real set

].(q - r),(q + r).[ is V134() V135() V136() open Element of K6(REAL)

Ball (q,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K7( the U1 of R^1, the U1 of m) is V16() set

K6(K7( the U1 of R^1, the U1 of m)) is set

K6( the U1 of m) is set

f is V16() Function-like V30( the U1 of R^1, the U1 of m) Element of K6(K7( the U1 of R^1, the U1 of m))

f1 is V11() real ext-real Element of the U1 of R^1

f . f1 is Element of the U1 of m

p is V1() V11() real ext-real positive non negative set

f1 - p is V11() real ext-real set

f1 + p is V11() real ext-real set

].(f1 - p),(f1 + p).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(f1 - p),(f1 + p).[ is Element of K6( the U1 of m)

q is V11() real ext-real Element of the U1 of RealSpace

Ball (q,p) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f .: (Ball (q,p)) is Element of K6( the U1 of m)

r is open Element of K6( the U1 of m)

q - p is V11() real ext-real set

q + p is V11() real ext-real set

].(q - p),(q + p).[ is V134() V135() V136() open Element of K6(REAL)

f1 is V11() real ext-real Element of the U1 of RealSpace

f . f1 is set

p is V1() V11() real ext-real positive non negative set

Ball (f1,p) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f .: (Ball (f1,p)) is Element of K6( the U1 of m)

q is V11() real ext-real Element of the U1 of R^1

f . q is Element of the U1 of m

f1 - p is V11() real ext-real set

f1 + p is V11() real ext-real set

].(f1 - p),(f1 + p).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(f1 - p),(f1 + p).[ is Element of K6( the U1 of m)

r is open Element of K6( the U1 of m)

K7( the U1 of R^1, the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of R^1, the U1 of R^1)) is set

m is V16() Function-like V30( the U1 of R^1, the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of R^1, the U1 of R^1))

f is V11() real ext-real Element of the U1 of R^1

m . f is V11() real ext-real Element of the U1 of R^1

f1 is V1() V11() real ext-real positive non negative set

f - f1 is V11() real ext-real set

f + f1 is V11() real ext-real set

].(f - f1),(f + f1).[ is V134() V135() V136() open Element of K6(REAL)

m .: ].(f - f1),(f + f1).[ is V134() V135() V136() Element of K6( the U1 of R^1)

q is V11() real ext-real Element of the U1 of RealSpace

p is V11() real ext-real Element of the U1 of RealSpace

Ball (p,f1) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m .: (Ball (p,f1)) is V134() V135() V136() Element of K6( the U1 of R^1)

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

(m . f) - r is V11() real ext-real set

(m . f) + r is V11() real ext-real set

].((m . f) - r),((m . f) + r).[ is V134() V135() V136() open Element of K6(REAL)

f1 is V11() real ext-real Element of the U1 of RealSpace

f is V11() real ext-real Element of the U1 of RealSpace

m . f is V11() real ext-real set

p is V1() V11() real ext-real positive non negative set

Ball (f,p) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m .: (Ball (f,p)) is V134() V135() V136() Element of K6( the U1 of R^1)

f - p is V11() real ext-real set

f + p is V11() real ext-real set

].(f - p),(f + p).[ is V134() V135() V136() open Element of K6(REAL)

m .: ].(f - p),(f + p).[ is V134() V135() V136() Element of K6( the U1 of R^1)

q is V1() V11() real ext-real positive non negative set

(m . f) - q is V11() real ext-real set

(m . f) + q is V11() real ext-real set

].((m . f) - q),((m . f) + q).[ is V134() V135() V136() open Element of K6(REAL)

Ball (f1,q) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

K7( the U1 of (TOP-REAL m), the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of (TOP-REAL m), the U1 of R^1)) is set

f is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of (TOP-REAL m), the U1 of R^1))

f1 is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

p is V1() V11() real ext-real positive non negative set

Ball (f1,p) is V1() open Element of K6( the U1 of (TOP-REAL m))

K6( the U1 of (TOP-REAL m)) is set

f . f1 is V11() real ext-real Element of the U1 of R^1

f .: (Ball (f1,p)) is V134() V135() V136() Element of K6( the U1 of R^1)

q is V11() real ext-real Element of REAL

(f . f1) - q is V11() real ext-real set

(f . f1) + q is V11() real ext-real set

].((f . f1) - q),((f . f1) + q).[ is V134() V135() V136() open Element of K6(REAL)

r is V1() V11() real ext-real positive non negative set

p1 is V1() V11() real ext-real positive non negative set

(f . f1) - p1 is V11() real ext-real set

(f . f1) + p1 is V11() real ext-real set

].((f . f1) - p1),((f . f1) + p1).[ is V134() V135() V136() open Element of K6(REAL)

f1 is Element of K6( the U1 of (TOP-REAL m))

f .: f1 is V134() V135() V136() Element of K6( the U1 of R^1)

p is set

q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f . q is V11() real ext-real Element of the U1 of R^1

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

the U1 of (Euclid m) is V1() set

Int f1 is Element of K6( the U1 of (TOP-REAL m))

r is Element of the U1 of (Euclid m)

p1 is V11() real ext-real set

Ball (r,p1) is Element of K6( the U1 of (Euclid m))

K6( the U1 of (Euclid m)) is set

Ball (q,p1) is open Element of K6( the U1 of (TOP-REAL m))

f .: (Ball (q,p1)) is V134() V135() V136() Element of K6( the U1 of R^1)

s is V1() V11() real ext-real positive non negative set

(f . q) - s is V11() real ext-real set

(f . q) + s is V11() real ext-real set

].((f . q) - s),((f . q) + s).[ is V134() V135() V136() open Element of K6(REAL)

R^1 ].((f . q) - s),((f . q) + s).[ is open V134() V135() V136() Element of K6( the U1 of K414())

c

q is V134() V135() V136() Element of K6( the U1 of R^1)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

K7( the U1 of R^1, the U1 of (TOP-REAL m)) is V16() set

K6(K7( the U1 of R^1, the U1 of (TOP-REAL m))) is set

f is V16() Function-like V30( the U1 of R^1, the U1 of (TOP-REAL m)) Element of K6(K7( the U1 of R^1, the U1 of (TOP-REAL m)))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))) is V16() set

K6(K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m)))) is set

p is V11() real ext-real Element of the U1 of R^1

f . p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

q is V1() V11() real ext-real positive non negative set

p - q is V11() real ext-real set

p + q is V11() real ext-real set

].(p - q),(p + q).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(p - q),(p + q).[ is Element of K6( the U1 of (TOP-REAL m))

f1 is V16() Function-like V30( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))) Element of K6(K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))))

p1 is Element of the U1 of (Euclid m)

r is V11() real ext-real Element of the U1 of RealSpace

Ball (r,q) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f1 .: (Ball (r,q)) is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

s is V1() V11() real ext-real positive non negative set

Ball (p1,s) is Element of K6( the U1 of (Euclid m))

Ball ((f . p),s) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 is V16() Function-like V30( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))) Element of K6(K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))))

p is V11() real ext-real Element of the U1 of RealSpace

f1 . p is set

q is Element of the U1 of (Euclid m)

r is V1() V11() real ext-real positive non negative set

Ball (p,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f1 .: (Ball (p,r)) is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

p1 is V11() real ext-real Element of the U1 of R^1

f . p1 is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

p1 - r is V11() real ext-real set

p1 + r is V11() real ext-real set

].(p1 - r),(p1 + r).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(p1 - r),(p1 + r).[ is Element of K6( the U1 of (TOP-REAL m))

s is V1() V11() real ext-real positive non negative set

Ball ((f . p1),s) is V1() open Element of K6( the U1 of (TOP-REAL m))

Ball (q,s) is Element of K6( the U1 of (Euclid m))

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K6( the U1 of m) is set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of m, the U1 of (TopSpaceMetr f)) is V16() set

K6(K7( the U1 of m, the U1 of (TopSpaceMetr f))) is set

f1 is V16() Function-like V30( the U1 of m, the U1 of (TopSpaceMetr f)) Element of K6(K7( the U1 of m, the U1 of (TopSpaceMetr f)))

p is Element of the U1 of m

f1 . p is Element of the U1 of (TopSpaceMetr f)

q is Element of the U1 of f

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is Element of K6( the U1 of f)

K6( the U1 of (TopSpaceMetr f)) is set

p1 is Element of K6( the U1 of (TopSpaceMetr f))

s is Element of K6( the U1 of m)

f1 .: s is Element of K6( the U1 of (TopSpaceMetr f))

K6( the U1 of (TopSpaceMetr f)) is set

p is Element of the U1 of m

f1 . p is Element of the U1 of (TopSpaceMetr f)

q is Element of K6( the U1 of (TopSpaceMetr f))

Int q is Element of K6( the U1 of (TopSpaceMetr f))

r is Element of the U1 of f

p1 is V11() real ext-real set

Ball (r,p1) is Element of K6( the U1 of f)

s is open Element of K6( the U1 of m)

f1 .: s is Element of K6( the U1 of (TopSpaceMetr f))

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K6( the U1 of m) is set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of (TopSpaceMetr f), the U1 of m) is V16() set

K6(K7( the U1 of (TopSpaceMetr f), the U1 of m)) is set

f1 is V16() Function-like V30( the U1 of (TopSpaceMetr f), the U1 of m) Element of K6(K7( the U1 of (TopSpaceMetr f), the U1 of m))

p is Element of the U1 of f

f1 . p is set

q is open Element of K6( the U1 of m)

K6( the U1 of (TopSpaceMetr f)) is set

r is Element of K6( the U1 of (TopSpaceMetr f))

f1 .: r is Element of K6( the U1 of m)

Int r is Element of K6( the U1 of (TopSpaceMetr f))

p1 is V11() real ext-real set

Ball (p,p1) is Element of K6( the U1 of f)

s is V1() V11() real ext-real positive non negative set

c

Ball (p,c

f1 .: (Ball (p,c

p is Element of the U1 of (TopSpaceMetr f)

f1 . p is Element of the U1 of m

q is Element of K6( the U1 of m)

r is Element of the U1 of f

p1 is V1() V11() real ext-real positive non negative set

Ball (r,p1) is Element of K6( the U1 of f)

f1 .: (Ball (r,p1)) is Element of K6( the U1 of m)

s is Element of K6( the U1 of (TopSpaceMetr f))

f1 .: s is Element of K6( the U1 of m)

m is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr m is non empty strict TopSpace-like TopStruct

the U1 of m is V1() set

Family_open_set m is Element of K6(K6( the U1 of m))

K6( the U1 of m) is set

K6(K6( the U1 of m)) is set

TopStruct(# the U1 of m,(Family_open_set m) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr m) is V1() set

f is non empty Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr f is non empty strict TopSpace-like TopStruct

the U1 of f is V1() set

Family_open_set f is Element of K6(K6( the U1 of f))

K6( the U1 of f) is set

K6(K6( the U1 of f)) is set

TopStruct(# the U1 of f,(Family_open_set f) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr f) is V1() set

K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)) is V16() set

K6(K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f))) is set

f1 is V16() Function-like V30( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)) Element of K6(K7( the U1 of (TopSpaceMetr m), the U1 of (TopSpaceMetr f)))

q is Element of the U1 of f

p is Element of the U1 of m

f1 . p is set

r is V1() V11() real ext-real positive non negative set

p1 is V11() real ext-real Element of REAL

s is V1() V11() real ext-real positive non negative set

c

Ball (p,c

f1 .: (Ball (p,c

K6( the U1 of (TopSpaceMetr f)) is set

Ball (q,r) is Element of K6( the U1 of f)

c

x is Element of the U1 of (TopSpaceMetr m)

f1 . x is Element of the U1 of (TopSpaceMetr f)

x1 is Element of the U1 of m

dist (p,x1) is V11() real ext-real Element of REAL

the distance of m is V16() Function-like V30(K7( the U1 of m, the U1 of m), REAL ) V124() V125() V126() Element of K6(K7(K7( the U1 of m, the U1 of m),REAL))

K7( the U1 of m, the U1 of m) is V16() set

K7(K7( the U1 of m, the U1 of m),REAL) is V16() V124() V125() V126() set

K6(K7(K7( the U1 of m, the U1 of m),REAL)) is set

the distance of m . (p,x1) is V11() real ext-real Element of REAL

y1 is Element of the U1 of f

dist (q,y1) is V11() real ext-real Element of REAL

the distance of f is V16() Function-like V30(K7( the U1 of f, the U1 of f), REAL ) V124() V125() V126() Element of K6(K7(K7( the U1 of f, the U1 of f),REAL))

K7( the U1 of f, the U1 of f) is V16() set

K7(K7( the U1 of f, the U1 of f),REAL) is V16() V124() V125() V126() set

K6(K7(K7( the U1 of f, the U1 of f),REAL)) is set

the distance of f . (q,y1) is V11() real ext-real Element of REAL

p is V11() real ext-real set

q is Element of the U1 of m

f1 . q is set

r is Element of the U1 of f

Ball (r,p) is Element of K6( the U1 of f)

p1 is V1() V11() real ext-real positive non negative set

Ball (q,p1) is Element of K6( the U1 of m)

f1 .: (Ball (q,p1)) is Element of K6( the U1 of (TopSpaceMetr f))

s is Element of the U1 of m

f1 . s is set

dist (q,s) is V11() real ext-real Element of REAL

the distance of m is V16() Function-like V30(K7( the U1 of m, the U1 of m), REAL ) V124() V125() V126() Element of K6(K7(K7( the U1 of m, the U1 of m),REAL))

K7( the U1 of m, the U1 of m) is V16() set

K7(K7( the U1 of m, the U1 of m),REAL) is V16() V124() V125() V126() set

K6(K7(K7( the U1 of m, the U1 of m),REAL)) is set

the distance of m . (q,s) is V11() real ext-real Element of REAL

c

dist (r,c

the distance of f is V16() Function-like V30(K7( the U1 of f, the U1 of f), REAL ) V124() V125() V126() Element of K6(K7(K7( the U1 of f, the U1 of f),REAL))

K7( the U1 of f, the U1 of f) is V16() set

K7(K7( the U1 of f, the U1 of f),REAL) is V16() V124() V125() V126() set

K6(K7(K7( the U1 of f, the U1 of f),REAL)) is set

the distance of f . (r,c

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is non empty TopSpace-like TopStruct

the U1 of f is V1() set

K7( the U1 of f, the U1 of (TOP-REAL m)) is V16() set

K6(K7( the U1 of f, the U1 of (TOP-REAL m))) is set

K6( the U1 of f) is set

f1 is V16() Function-like V30( the U1 of f, the U1 of (TOP-REAL m)) Element of K6(K7( the U1 of f, the U1 of (TOP-REAL m)))

p is Element of the U1 of f

f1 . p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

q is V1() V11() real ext-real positive non negative set

Ball ((f1 . p),q) is V1() open Element of K6( the U1 of (TOP-REAL m))

K6( the U1 of (TOP-REAL m)) is set

r is Element of K6( the U1 of f)

f1 .: r is Element of K6( the U1 of (TOP-REAL m))

K6( the U1 of (TOP-REAL m)) is set

p is Element of the U1 of f

f1 . p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

q is Element of K6( the U1 of (TOP-REAL m))

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

the U1 of (Euclid m) is V1() set

Int q is Element of K6( the U1 of (TOP-REAL m))

r is Element of the U1 of (Euclid m)

p1 is V11() real ext-real set

Ball (r,p1) is Element of K6( the U1 of (Euclid m))

K6( the U1 of (Euclid m)) is set

Ball ((f1 . p),p1) is open Element of K6( the U1 of (TOP-REAL m))

s is open Element of K6( the U1 of f)

f1 .: s is Element of K6( the U1 of (TOP-REAL m))

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is non empty TopSpace-like TopStruct

the U1 of f is V1() set

K7( the U1 of (TOP-REAL m), the U1 of f) is V16() set

K6(K7( the U1 of (TOP-REAL m), the U1 of f)) is set

K6( the U1 of f) is set

f1 is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of f) Element of K6(K7( the U1 of (TOP-REAL m), the U1 of f))

p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . p is Element of the U1 of f

q is open Element of K6( the U1 of f)

K6( the U1 of (TOP-REAL m)) is set

r is Element of K6( the U1 of (TOP-REAL m))

f1 .: r is Element of K6( the U1 of f)

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

the U1 of (Euclid m) is V1() set

Int r is Element of K6( the U1 of (TOP-REAL m))

p1 is Element of the U1 of (Euclid m)

s is V11() real ext-real set

Ball (p1,s) is Element of K6( the U1 of (Euclid m))

K6( the U1 of (Euclid m)) is set

c

c

Ball (p1,c

Ball (p,c

f1 .: (Ball (p,c

p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . p is Element of the U1 of f

q is Element of K6( the U1 of f)

r is V1() V11() real ext-real positive non negative set

Ball (p,r) is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: (Ball (p,r)) is Element of K6( the U1 of f)

p1 is V1() open Element of K6( the U1 of (TOP-REAL m))

f1 .: p1 is Element of K6( the U1 of f)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

f is natural V11() real ext-real set

TOP-REAL f is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL f) is V1() set

K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)) is V16() set

K6(K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f))) is set

f1 is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)) Element of K6(K7( the U1 of (TOP-REAL m), the U1 of (TOP-REAL f)))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the topology of (TOP-REAL f) is V1() Element of K6(K6( the U1 of (TOP-REAL f)))

K6( the U1 of (TOP-REAL f)) is set

K6(K6( the U1 of (TOP-REAL f))) is set

TopStruct(# the U1 of (TOP-REAL f), the topology of (TOP-REAL f) #) is non empty strict TopSpace-like TopStruct

Euclid f is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid f) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid f) is V1() set

Family_open_set (Euclid f) is Element of K6(K6( the U1 of (Euclid f)))

K6( the U1 of (Euclid f)) is set

K6(K6( the U1 of (Euclid f))) is set

TopStruct(# the U1 of (Euclid f),(Family_open_set (Euclid f)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

the U1 of (TopSpaceMetr (Euclid f)) is V1() set

K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))) is V16() set

K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f)))) is set

q is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . q is V42(f) V43() V126() Element of the U1 of (TOP-REAL f)

p is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))) Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of (TopSpaceMetr (Euclid f))))

p1 is Element of the U1 of (Euclid m)

s is Element of the U1 of (Euclid f)

r is V1() V11() real ext-real positive non negative set

Ball (s,r) is Element of K6( the U1 of (Euclid f))

c

Ball (p1,c

p .: (Ball (p1,c

K6( the U1 of (TopSpaceMetr (Euclid f))) is set

c

Ball (p1,c

Ball (q,c

Ball ((f1 . q),r) is V1() open Element of K6( the U1 of (TOP-REAL f))

f1 .: (Ball (q,c

q is Element of the U1 of (Euclid m)

p . q is set

r is Element of the U1 of (Euclid f)

p1 is V1() V11() real ext-real positive non negative set

Ball (r,p1) is Element of K6( the U1 of (Euclid f))

s is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 . s is V42(f) V43() V126() Element of the U1 of (TOP-REAL f)

Ball ((f1 . s),p1) is V1() open Element of K6( the U1 of (TOP-REAL f))

c

Ball (s,c

f1 .: (Ball (s,c

Ball (q,c

p .: (Ball (q,c

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K7( the U1 of m, the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of m, the U1 of R^1)) is set

K6( the U1 of m) is set

f is V16() Function-like V30( the U1 of m, the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of m, the U1 of R^1))

f1 is Element of the U1 of m

f . f1 is V11() real ext-real Element of the U1 of R^1

p is V1() V11() real ext-real positive non negative set

(f . f1) - p is V11() real ext-real set

(f . f1) + p is V11() real ext-real set

].((f . f1) - p),((f . f1) + p).[ is V134() V135() V136() open Element of K6(REAL)

R^1 ].((f . f1) - p),((f . f1) + p).[ is open V134() V135() V136() Element of K6( the U1 of K414())

q is Element of K6( the U1 of m)

f .: q is V134() V135() V136() Element of K6( the U1 of R^1)

f1 is Element of the U1 of m

f . f1 is V11() real ext-real Element of the U1 of R^1

p is V134() V135() V136() Element of K6( the U1 of R^1)

q is V11() real ext-real Element of REAL

(f . f1) - q is V11() real ext-real set

(f . f1) + q is V11() real ext-real set

].((f . f1) - q),((f . f1) + q).[ is V134() V135() V136() open Element of K6(REAL)

r is open Element of K6( the U1 of m)

f .: r is V134() V135() V136() Element of K6( the U1 of R^1)

m is non empty TopSpace-like TopStruct

the U1 of m is V1() set

K7( the U1 of R^1, the U1 of m) is V16() set

K6(K7( the U1 of R^1, the U1 of m)) is set

K6( the U1 of m) is set

f is V16() Function-like V30( the U1 of R^1, the U1 of m) Element of K6(K7( the U1 of R^1, the U1 of m))

f1 is V11() real ext-real Element of the U1 of R^1

f . f1 is Element of the U1 of m

p is open Element of K6( the U1 of m)

q is V134() V135() V136() Element of K6( the U1 of R^1)

f .: q is Element of K6( the U1 of m)

r is V11() real ext-real Element of REAL

f1 - r is V11() real ext-real set

f1 + r is V11() real ext-real set

].(f1 - r),(f1 + r).[ is V134() V135() V136() open Element of K6(REAL)

p1 is V1() V11() real ext-real positive non negative set

s is V1() V11() real ext-real positive non negative set

f1 - s is V11() real ext-real set

f1 + s is V11() real ext-real set

].(f1 - s),(f1 + s).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(f1 - s),(f1 + s).[ is Element of K6( the U1 of m)

f1 is V11() real ext-real Element of the U1 of R^1

f . f1 is Element of the U1 of m

p is Element of K6( the U1 of m)

q is V1() V11() real ext-real positive non negative set

f1 - q is V11() real ext-real set

f1 + q is V11() real ext-real set

].(f1 - q),(f1 + q).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(f1 - q),(f1 + q).[ is Element of K6( the U1 of m)

R^1 ].(f1 - q),(f1 + q).[ is open V134() V135() V136() Element of K6( the U1 of K414())

r is open V134() V135() V136() Element of K6( the U1 of K414())

f .: r is Element of K6( the U1 of m)

m is V16() Function-like V30( the U1 of R^1, the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of R^1, the U1 of R^1))

f is V11() real ext-real Element of the U1 of R^1

m . f is V11() real ext-real Element of the U1 of R^1

p is V11() real ext-real Element of the U1 of RealSpace

q is V11() real ext-real Element of the U1 of RealSpace

f1 is V1() V11() real ext-real positive non negative set

Ball (q,f1) is V134() V135() V136() Element of K6( the U1 of RealSpace)

r is V1() V11() real ext-real positive non negative set

Ball (p,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m .: (Ball (p,r)) is V134() V135() V136() Element of K6( the U1 of R^1)

p1 is V1() V11() real ext-real positive non negative set

Ball (p,p1) is V134() V135() V136() Element of K6( the U1 of RealSpace)

p - p1 is V11() real ext-real set

p + p1 is V11() real ext-real set

].(p - p1),(p + p1).[ is V134() V135() V136() open Element of K6(REAL)

q - f1 is V11() real ext-real set

q + f1 is V11() real ext-real set

].(q - f1),(q + f1).[ is V134() V135() V136() open Element of K6(REAL)

f - p1 is V11() real ext-real set

f + p1 is V11() real ext-real set

].(f - p1),(f + p1).[ is V134() V135() V136() open Element of K6(REAL)

m .: ].(f - p1),(f + p1).[ is V134() V135() V136() Element of K6( the U1 of R^1)

(m . f) - f1 is V11() real ext-real set

(m . f) + f1 is V11() real ext-real set

].((m . f) - f1),((m . f) + f1).[ is V134() V135() V136() open Element of K6(REAL)

f1 is V11() real ext-real Element of the U1 of RealSpace

f is V11() real ext-real Element of the U1 of RealSpace

m . f is V11() real ext-real set

p is V1() V11() real ext-real positive non negative set

Ball (f1,p) is V134() V135() V136() Element of K6( the U1 of RealSpace)

(m . f) - p is V11() real ext-real set

(m . f) + p is V11() real ext-real set

].((m . f) - p),((m . f) + p).[ is V134() V135() V136() open Element of K6(REAL)

q is V1() V11() real ext-real positive non negative set

f - q is V11() real ext-real set

f + q is V11() real ext-real set

].(f - q),(f + q).[ is V134() V135() V136() open Element of K6(REAL)

m .: ].(f - q),(f + q).[ is V134() V135() V136() Element of K6( the U1 of R^1)

Ball (f,q) is V134() V135() V136() Element of K6( the U1 of RealSpace)

m .: (Ball (f,q)) is V134() V135() V136() Element of K6( the U1 of R^1)

f1 - p is V11() real ext-real set

f1 + p is V11() real ext-real set

].(f1 - p),(f1 + p).[ is V134() V135() V136() open Element of K6(REAL)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

K7( the U1 of (TOP-REAL m), the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of (TOP-REAL m), the U1 of R^1)) is set

f is V16() Function-like V30( the U1 of (TOP-REAL m), the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of (TOP-REAL m), the U1 of R^1))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of R^1) is V16() V124() V125() V126() set

K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of R^1)) is set

p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f . p is V11() real ext-real Element of the U1 of R^1

f1 is V16() Function-like V30( the U1 of (TopSpaceMetr (Euclid m)), the U1 of R^1) V124() V125() V126() Element of K6(K7( the U1 of (TopSpaceMetr (Euclid m)), the U1 of R^1))

r is Element of the U1 of (Euclid m)

p1 is V11() real ext-real Element of the U1 of RealSpace

q is V1() V11() real ext-real positive non negative set

Ball (p1,q) is V134() V135() V136() Element of K6( the U1 of RealSpace)

s is V1() V11() real ext-real positive non negative set

Ball (r,s) is Element of K6( the U1 of (Euclid m))

f .: (Ball (r,s)) is V134() V135() V136() Element of K6( the U1 of R^1)

c

Ball (r,c

Ball (p,c

(f . p) - q is V11() real ext-real set

(f . p) + q is V11() real ext-real set

].((f . p) - q),((f . p) + q).[ is V134() V135() V136() open Element of K6(REAL)

f .: (Ball (p,c

p is Element of the U1 of (Euclid m)

f1 . p is V11() real ext-real set

q is V11() real ext-real Element of the U1 of RealSpace

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is V134() V135() V136() Element of K6( the U1 of RealSpace)

p1 is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f . p is V11() real ext-real set

(f . p) - r is V11() real ext-real set

(f . p) + r is V11() real ext-real set

].((f . p) - r),((f . p) + r).[ is V134() V135() V136() open Element of K6(REAL)

s is V1() V11() real ext-real positive non negative set

Ball (p1,s) is V1() open Element of K6( the U1 of (TOP-REAL m))

f .: (Ball (p1,s)) is V134() V135() V136() Element of K6( the U1 of R^1)

Ball (p,s) is Element of K6( the U1 of (Euclid m))

f1 .: (Ball (p,s)) is V134() V135() V136() Element of K6( the U1 of R^1)

m is natural V11() real ext-real set

TOP-REAL m is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

the U1 of (TOP-REAL m) is V1() set

K7( the U1 of R^1, the U1 of (TOP-REAL m)) is V16() set

K6(K7( the U1 of R^1, the U1 of (TOP-REAL m))) is set

f is V16() Function-like V30( the U1 of R^1, the U1 of (TOP-REAL m)) Element of K6(K7( the U1 of R^1, the U1 of (TOP-REAL m)))

the topology of (TOP-REAL m) is V1() Element of K6(K6( the U1 of (TOP-REAL m)))

K6( the U1 of (TOP-REAL m)) is set

K6(K6( the U1 of (TOP-REAL m))) is set

TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) is non empty strict TopSpace-like TopStruct

Euclid m is non empty strict Reflexive discerning V83() triangle Discerning MetrStruct

TopSpaceMetr (Euclid m) is non empty strict TopSpace-like TopStruct

the U1 of (Euclid m) is V1() set

Family_open_set (Euclid m) is Element of K6(K6( the U1 of (Euclid m)))

K6( the U1 of (Euclid m)) is set

K6(K6( the U1 of (Euclid m))) is set

TopStruct(# the U1 of (Euclid m),(Family_open_set (Euclid m)) #) is non empty strict TopStruct

the U1 of (TopSpaceMetr (Euclid m)) is V1() set

K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))) is V16() set

K6(K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m)))) is set

p is V11() real ext-real Element of the U1 of R^1

f . p is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

f1 is V16() Function-like V30( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))) Element of K6(K7( the U1 of R^1, the U1 of (TopSpaceMetr (Euclid m))))

r is V11() real ext-real Element of the U1 of RealSpace

p1 is Element of the U1 of (Euclid m)

q is V1() V11() real ext-real positive non negative set

Ball (p1,q) is Element of K6( the U1 of (Euclid m))

s is V1() V11() real ext-real positive non negative set

Ball (r,s) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f1 .: (Ball (r,s)) is Element of K6( the U1 of (TopSpaceMetr (Euclid m)))

K6( the U1 of (TopSpaceMetr (Euclid m))) is set

c

Ball (r,c

p - c

p + c

].(p - c

Ball ((f . p),q) is V1() open Element of K6( the U1 of (TOP-REAL m))

f .: ].(p - c

p is V11() real ext-real Element of the U1 of RealSpace

f . p is set

q is Element of the U1 of (Euclid m)

r is V1() V11() real ext-real positive non negative set

Ball (q,r) is Element of K6( the U1 of (Euclid m))

p1 is V11() real ext-real Element of the U1 of R^1

f . p1 is V42(m) V43() V126() Element of the U1 of (TOP-REAL m)

Ball ((f . p1),r) is V1() open Element of K6( the U1 of (TOP-REAL m))

s is V1() V11() real ext-real positive non negative set

p - s is V11() real ext-real set

p + s is V11() real ext-real set

].(p - s),(p + s).[ is V134() V135() V136() open Element of K6(REAL)

f .: ].(p - s),(p + s).[ is Element of K6( the U1 of (TOP-REAL m))

Ball (p,s) is V134() V135() V136() Element of K6( the U1 of RealSpace)

f .: (Ball (p,s)) is Element of K6( the U1 of (TOP-REAL m))