:: 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₉ is V1() V11() real ext-real positive non negative set
Ball (r,c₉) 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 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₉ is V1() V11() real ext-real positive non negative set
Ball (s,c₉) is Element of K6( the U1 of (Euclid f))
Ball ((f1 . q),c₉) is V1() open 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))))
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₉ is V42(f) V43() V126() Element of the U1 of (TOP-REAL f)
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₁₀ is V1() V11() real ext-real positive non negative set
Ball (c₉,c₁₀) is V1() open Element of K6( the U1 of (TOP-REAL f))
Ball (r,c₁₀) is Element of K6( the U1 of (Euclid f))
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₉ is open V134() V135() V136() Element of K6( the U1 of K414())
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₉ is V1() V11() real ext-real positive non negative set
Ball (p,c₉) is Element of K6( the U1 of f)
f1 .: (Ball (p,c₉)) 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 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₉ is V1() V11() real ext-real positive non negative set
Ball (p,c₉) is Element of K6( the U1 of m)
f1 .: (Ball (p,c₉)) is Element of K6( the U1 of (TopSpaceMetr f))
K6( the U1 of (TopSpaceMetr f)) is set
Ball (q,r) is Element of K6( the U1 of f)
c₁₀ is set
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₉ is Element of the U1 of f
dist (r,c₉) 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 . (r,c₉) is V11() real ext-real Element of 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
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₉ is V1() V11() real ext-real positive non negative set
c₁₀ is V1() V11() real ext-real positive non negative set
Ball (p1,c₁₀) is Element of K6( the U1 of (Euclid m))
Ball (p,c₁₀) is V1() open Element of K6( the U1 of (TOP-REAL m))
f1 .: (Ball (p,c₁₀)) is Element of K6( 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 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₉ is V1() V11() real ext-real positive non negative set
Ball (p1,c₉) is Element of K6( the U1 of (Euclid m))
p .: (Ball (p1,c₉)) is Element of K6( the U1 of (TopSpaceMetr (Euclid f)))
K6( the U1 of (TopSpaceMetr (Euclid f))) is set
c₁₀ is V1() V11() real ext-real positive non negative set
Ball (p1,c₁₀) is Element of K6( the U1 of (Euclid m))
Ball (q,c₁₀) is V1() open Element of K6( the U1 of (TOP-REAL m))
Ball ((f1 . q),r) is V1() open Element of K6( the U1 of (TOP-REAL f))
f1 .: (Ball (q,c₁₀)) is Element of K6( the U1 of (TOP-REAL 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 (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₉ is V1() V11() real ext-real positive non negative set
Ball (s,c₉) is V1() open Element of K6( the U1 of (TOP-REAL m))
f1 .: (Ball (s,c₉)) is Element of K6( the U1 of (TOP-REAL f))
Ball (q,c₉) is Element of K6( the U1 of (Euclid m))
p .: (Ball (q,c₉)) is Element of K6( the U1 of (TopSpaceMetr (Euclid f)))
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₉ is V1() V11() real ext-real positive non negative set
Ball (r,c₉) is Element of K6( the U1 of (Euclid m))
Ball (p,c₉) is V1() open Element of K6( the U1 of (TOP-REAL m))
(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₉)) is V134() V135() V136() Element of K6( the U1 of R^1)
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₉ is V1() V11() real ext-real positive non negative set
Ball (r,c₉) is V134() V135() V136() Element of K6( the U1 of RealSpace)
p - c₉ is V11() real ext-real set
p + c₉ is V11() real ext-real set
].(p - c₉),(p + c₉).[ is V134() V135() V136() open Element of K6(REAL)
Ball ((f . p),q) is V1() open Element of K6( the U1 of (TOP-REAL m))
f .: ].(p - c₉),(p + c₉).[ is Element of K6( the U1 of (TOP-REAL m))
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))