:: COMPL_SP semantic presentation

REAL is non empty non trivial non finite V141() V142() V143() V147() set

NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V141() V142() V143() V144() V145() V146() V147() Element of bool REAL

bool REAL is non empty non trivial non finite set

K246() is V141() V142() V143() Element of bool REAL

omega is non empty non trivial ordinal non finite cardinal limit_cardinal V141() V142() V143() V144() V145() V146() V147() set

bool omega is non empty non trivial non finite set

1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

[:1,1:] is non empty finite set

bool [:1,1:] is non empty finite V34() set

[:[:1,1:],1:] is non empty finite set

bool [:[:1,1:],1:] is non empty finite V34() set

[:[:1,1:],REAL:] is non empty non trivial non finite set

bool [:[:1,1:],REAL:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

2 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

[:2,2:] is non empty finite set

[:[:2,2:],REAL:] is non empty non trivial non finite set

bool [:[:2,2:],REAL:] is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite V141() V147() set

bool NAT is non empty non trivial non finite set

K314() is V137() TopStruct

the carrier of K314() is V141() V142() V143() set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V137() MetrStruct

real_dist is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V27([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

K319() is non empty strict TopSpace-like V137() TopStruct

K247() is V141() V142() V143() Element of bool REAL

ExtREAL is non empty V142() set

bool ExtREAL is non empty set

the carrier of K319() is non empty V141() V142() V143() set

[:NAT,REAL:] is non empty non trivial non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

RAT is non empty non trivial non finite V141() V142() V143() V144() V147() set

INT is non empty non trivial non finite V141() V142() V143() V144() V145() V147() set

0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() set

{0,1} is non empty finite V34() V141() V142() V143() V144() V145() V146() set

bool (bool REAL) is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is non empty non trivial non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is non empty non trivial non finite set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is non empty non trivial non finite set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is non empty non trivial non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is non empty non trivial non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT

4 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

card 0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() set

card omega is non empty non trivial ordinal non finite cardinal set

D is non empty MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is set

b is Element of the carrier of D

{b} is non empty trivial finite 1 -element Element of bool the carrier of D

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

X is Element of bool the carrier of D

NAT --> X is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

TW is Element of the carrier of D

f is Element of the carrier of D

dist (TW,f) is V11() real ext-real Element of REAL

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . (TW,f) is V11() real ext-real Element of REAL

TW is ordinal natural V11() real finite cardinal ext-real non negative set

f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

W . f is Element of bool the carrier of D

W . TW is Element of bool the carrier of D

dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is set

W . TW is set

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

b is set

X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

W is ordinal natural V11() real finite cardinal ext-real non negative set

a . W is Element of bool the carrier of D

diameter (a . W) is V11() real ext-real Element of REAL

b is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

X is ordinal natural V11() real finite cardinal ext-real non negative set

b . X is V11() real ext-real Element of REAL

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

b is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . W is V11() real ext-real Element of REAL

a . W is Element of bool the carrier of D

diameter (a . W) is V11() real ext-real Element of REAL

X . W is V11() real ext-real Element of REAL

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

(D,a) . X is V11() real ext-real Element of REAL

- 1 is V11() real ext-real non positive Element of REAL

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

(D,a) . 0 is V11() real ext-real Element of REAL

((D,a) . 0) + 1 is V11() real ext-real Element of REAL

((D,a) . 0) + 0 is V11() real ext-real Element of REAL

X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

(D,a) . X is V11() real ext-real Element of REAL

a . 0 is Element of bool the carrier of D

diameter (a . 0) is V11() real ext-real Element of REAL

X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

dom (D,a) is V141() V142() V143() V144() V145() V146() Element of bool NAT

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

(D,a) . X is V11() real ext-real Element of REAL

a . W is Element of bool the carrier of D

diameter (a . W) is V11() real ext-real Element of REAL

(D,a) . W is V11() real ext-real Element of REAL

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

dom (D,a) is V141() V142() V143() V144() V145() V146() Element of bool NAT

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . W is Element of bool the carrier of D

a . X is Element of bool the carrier of D

diameter (a . X) is V11() real ext-real Element of REAL

(D,a) . X is V11() real ext-real Element of REAL

diameter (a . W) is V11() real ext-real Element of REAL

(D,a) . W is V11() real ext-real Element of REAL

D is non empty Reflexive MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

[:NAT, the carrier of D:] is non empty non trivial non finite set

bool [:NAT, the carrier of D:] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

lim (D,a) is V11() real ext-real Element of REAL

X is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]

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

TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

X . f is Element of the carrier of D

X . s is Element of the carrier of D

dist ((X . f),(X . s)) is V11() real ext-real Element of REAL

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . ((X . f),(X . s)) is V11() real ext-real Element of REAL

a . s is Element of bool the carrier of D

a . TW is Element of bool the carrier of D

X . s is Element of the carrier of D

X . f is Element of the carrier of D

a . f is Element of bool the carrier of D

(D,a) . TW is V11() real ext-real Element of REAL

((D,a) . TW) - 0 is V11() real ext-real Element of REAL

abs (((D,a) . TW) - 0) is V11() real ext-real Element of REAL

diameter (a . TW) is V11() real ext-real Element of REAL

dist ((X . f),(X . s)) is V11() real ext-real Element of REAL

the distance of D . ((X . f),(X . s)) is V11() real ext-real Element of REAL

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

2 * D is V11() real ext-real Element of REAL

a is non empty Reflexive symmetric triangle MetrStruct

the carrier of a is non empty set

b is Element of the carrier of a

cl_Ball (b,D) is Element of bool the carrier of a

bool the carrier of a is non empty set

diameter (cl_Ball (b,D)) is V11() real ext-real Element of REAL

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

the distance of a is non empty Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like total V27([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty non trivial non finite set

the distance of a . (b,b) is V11() real ext-real Element of REAL

X is Element of the carrier of a

W is Element of the carrier of a

dist (X,b) is V11() real ext-real Element of REAL

the distance of a . (X,b) is V11() real ext-real Element of REAL

dist (X,W) is V11() real ext-real Element of REAL

the distance of a . (X,W) is V11() real ext-real Element of REAL

dist (b,W) is V11() real ext-real Element of REAL

the distance of a . (b,W) is V11() real ext-real Element of REAL

(dist (X,b)) + (dist (b,W)) is V11() real ext-real Element of REAL

D + D is V11() real ext-real Element of REAL

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

a is Element of bool the carrier of D

TopSpaceMetr D is strict TopSpace-like TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct

a is Element of bool the carrier of D

[#] D is non proper Element of bool the carrier of D

a ` is Element of bool the carrier of D

the carrier of D \ a is set

Family_open_set D is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

D is non empty MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

[#] D is non empty non proper Element of bool the carrier of D

Family_open_set D is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

{} D is empty trivial proper ordinal natural V11() real finite V34() cardinal 0 -element bounded ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() (D) (D) Element of bool the carrier of D

({} D) ` is Element of bool the carrier of D

the carrier of D \ ({} D) is set

(({} D) `) ` is Element of bool the carrier of D

the carrier of D \ (({} D) `) is set

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

TopSpaceMetr D is strict TopSpace-like TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct

the carrier of (TopSpaceMetr D) is set

bool the carrier of (TopSpaceMetr D) is non empty set

a is Element of bool the carrier of D

b is Element of bool the carrier of (TopSpaceMetr D)

a ` is Element of bool the carrier of D

the carrier of D \ a is set

b ` is Element of bool the carrier of (TopSpaceMetr D)

the carrier of (TopSpaceMetr D) \ b is set

a ` is Element of bool the carrier of D

the carrier of D \ a is set

D is TopStruct

the carrier of D is set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

[#] D is non proper open closed Element of bool the carrier of D

NAT --> ([#] D) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

a is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

b is ordinal natural V11() real finite cardinal ext-real non negative set

a . b is Element of bool the carrier of D

b is ordinal natural V11() real finite cardinal ext-real non negative set

a . b is Element of bool the carrier of D

dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT

b is set

a . b is set

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is set

b is Element of the carrier of D

Ball (b,1) is bounded Element of bool the carrier of D

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

NAT --> (Ball (b,1)) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

TW is set

dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT

f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

W . f is Element of bool the carrier of D

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

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . (b,b) is V11() real ext-real Element of REAL

W . TW is set

TW is ordinal natural V11() real finite cardinal ext-real non negative set

W . TW is Element of bool the carrier of D

Family_open_set D is Element of bool (bool the carrier of D)

TW is ordinal natural V11() real finite cardinal ext-real non negative set

W . TW is Element of bool the carrier of D

a is set

b is Element of the carrier of D

cl_Ball (b,1) is Element of bool the carrier of D

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

NAT --> (cl_Ball (b,1)) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

TW is set

dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT

f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

W . f is Element of bool the carrier of D

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

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . (b,b) is V11() real ext-real Element of REAL

W . TW is set

TW is ordinal natural V11() real finite cardinal ext-real non negative set

W . TW is Element of bool the carrier of D

[#] D is non empty non proper Element of bool the carrier of D

([#] D) \ (cl_Ball (b,1)) is Element of bool the carrier of D

Family_open_set D is Element of bool (bool the carrier of D)

(cl_Ball (b,1)) ` is Element of bool the carrier of D

the carrier of D \ (cl_Ball (b,1)) is set

TW is ordinal natural V11() real finite cardinal ext-real non negative set

W . TW is Element of bool the carrier of D

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

TopSpaceMetr D is strict TopSpace-like TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct

the carrier of (TopSpaceMetr D) is set

bool the carrier of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))

bool the carrier of (TopSpaceMetr D) is non empty set

bool (bool the carrier of (TopSpaceMetr D)) is non empty set

[:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

b is non empty Relation-like NAT -defined bool the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr D)) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr D)):]

X is ordinal natural V11() real finite cardinal ext-real non negative set

b . X is Element of bool the carrier of (TopSpaceMetr D)

a . X is Element of bool the carrier of D

X is ordinal natural V11() real finite cardinal ext-real non negative set

a . X is Element of bool the carrier of D

b . X is Element of bool the carrier of (TopSpaceMetr D)

X is ordinal natural V11() real finite cardinal ext-real non negative set

b . X is Element of bool the carrier of (TopSpaceMetr D)

a . X is Element of bool the carrier of D

X is ordinal natural V11() real finite cardinal ext-real non negative set

a . X is Element of bool the carrier of D

b . X is Element of bool the carrier of (TopSpaceMetr D)

D is non empty Reflexive symmetric triangle MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

TopSpaceMetr D is non empty strict TopSpace-like TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr D) is non empty set

bool the carrier of (TopSpaceMetr D) is non empty set

a is Element of bool the carrier of D

b is Element of bool the carrier of D

diameter a is V11() real ext-real Element of REAL

diameter b is V11() real ext-real Element of REAL

TW is Element of bool the carrier of (TopSpaceMetr D)

Cl TW is closed Element of bool the carrier of (TopSpaceMetr D)

f is Element of the carrier of D

s is Element of the carrier of D

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

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . (f,s) is V11() real ext-real Element of REAL

(dist (f,s)) - (diameter a) is V11() real ext-real Element of REAL

((dist (f,s)) - (diameter a)) / 2 is V11() real ext-real Element of REAL

Ball (f,(((dist (f,s)) - (diameter a)) / 2)) is bounded Element of bool the carrier of D

Ball (s,(((dist (f,s)) - (diameter a)) / 2)) is bounded Element of bool the carrier of D

(diameter a) - (diameter a) is V11() real ext-real Element of REAL

0 / 2 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of REAL

SI is Element of bool the carrier of (TopSpaceMetr D)

c

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

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

rngs is Element of the carrier of (TopSpaceMetr D)

x is set

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

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

S is Element of the carrier of (TopSpaceMetr D)

y is set

xS is Element of the carrier of D

dist (f,xS) is V11() real ext-real Element of REAL

the distance of D . (f,xS) is V11() real ext-real Element of REAL

j1 is Element of the carrier of D

dist (xS,j1) is V11() real ext-real Element of REAL

the distance of D . (xS,j1) is V11() real ext-real Element of REAL

(((dist (f,s)) - (diameter a)) / 2) + (diameter a) is V11() real ext-real Element of REAL

(dist (f,xS)) + (dist (xS,j1)) is V11() real ext-real Element of REAL

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

the distance of D . (s,j1) is V11() real ext-real Element of REAL

dist (f,j1) is V11() real ext-real Element of REAL

the distance of D . (f,j1) is V11() real ext-real Element of REAL

((((dist (f,s)) - (diameter a)) / 2) + (diameter a)) + (((dist (f,s)) - (diameter a)) / 2) is V11() real ext-real Element of REAL

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

the distance of D . (j1,s) is V11() real ext-real Element of REAL

(dist (f,j1)) + (dist (j1,s)) is V11() real ext-real Element of REAL

(diameter a) + 1 is V11() real ext-real Element of REAL

(diameter a) + 0 is V11() real ext-real Element of REAL

f is Element of the carrier of D

s is Element of the carrier of D

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

the distance of D . (f,s) is V11() real ext-real Element of REAL

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

s is Element of the carrier of D

S is Element of the carrier of D

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

the distance of D . (s,S) is V11() real ext-real Element of REAL

0 + 0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT

D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of D is non empty set

[:NAT, the carrier of D:] is non empty non trivial non finite set

bool [:NAT, the carrier of D:] is non empty non trivial non finite set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr D) is non empty set

bool the carrier of (TopSpaceMetr D) is non empty set

b is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]

X is set

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

f is set

s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . s is Element of the carrier of D

f is Element of bool the carrier of (TopSpaceMetr D)

Cl f is closed Element of bool the carrier of (TopSpaceMetr D)

s is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

X is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

W is set

dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

X . TW is Element of bool the carrier of D

f is Element of bool the carrier of (TopSpaceMetr D)

Cl f is closed Element of bool the carrier of (TopSpaceMetr D)

b . TW is Element of the carrier of D

X . W is set

W is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

X . W is Element of bool the carrier of D

TW is Element of bool the carrier of (TopSpaceMetr D)

Cl TW is closed Element of bool the carrier of (TopSpaceMetr D)

W is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,W) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

lim (D,W) is V11() real ext-real Element of REAL

TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

W . TW is Element of bool the carrier of D

f is Element of bool the carrier of (TopSpaceMetr D)

Cl f is closed Element of bool the carrier of (TopSpaceMetr D)

TW + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

W . (TW + 1) is Element of bool the carrier of D

s is Element of bool the carrier of (TopSpaceMetr D)

Cl s is closed Element of bool the carrier of (TopSpaceMetr D)

S is set

rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . rngs is Element of the carrier of D

TW is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

W . TW is Element of bool the carrier of D

f is Element of bool the carrier of (TopSpaceMetr D)

Cl f is closed Element of bool the carrier of (TopSpaceMetr D)

rng b is Element of bool the carrier of D

S is set

dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT

rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . rngs is Element of the carrier of D

s is Element of bool the carrier of D

TW is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,TW) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

s is V11() real ext-real set

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

S / 2 is V11() real ext-real Element of REAL

F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

(D,TW) . F is V11() real ext-real Element of REAL

((D,TW) . F) - 0 is V11() real ext-real Element of REAL

abs (((D,TW) . F) - 0) is V11() real ext-real Element of REAL

{ (b . b

W . F is Element of bool the carrier of D

R is Element of bool the carrier of (TopSpaceMetr D)

Cl R is closed Element of bool the carrier of (TopSpaceMetr D)

R9 is Element of the carrier of D

R9 is Element of bool the carrier of D

c

SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . SI is Element of the carrier of D

x is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . x is Element of the carrier of D

dist (R9,c

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . (R9,c

R9 is set

dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT

c

b . c

diameter R9 is V11() real ext-real Element of REAL

diameter (W . F) is V11() real ext-real Element of REAL

b . F is Element of the carrier of D

abs (diameter (W . F)) is V11() real ext-real Element of REAL

TW is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

W . TW is Element of bool the carrier of D

D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct

b is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,b) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

lim (D,b) is V11() real ext-real Element of REAL

meet b is Element of bool the carrier of D

dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT

X is set

b . X is set

rng b is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

W is set

[:NAT, the carrier of D:] is non empty non trivial non finite set

bool [:NAT, the carrier of D:] is non empty non trivial non finite set

X is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]

W is ordinal natural V11() real finite cardinal ext-real non negative set

X . W is Element of the carrier of D

b . W is Element of bool the carrier of D

W is Element of the carrier of D

the carrier of (TopSpaceMetr D) is non empty set

[:NAT, the carrier of (TopSpaceMetr D):] is non empty non trivial non finite set

bool [:NAT, the carrier of (TopSpaceMetr D):] is non empty non trivial non finite set

TW is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , the carrier of (TopSpaceMetr D)) Element of bool [:NAT, the carrier of (TopSpaceMetr D):]

s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

TW ^\ s is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , the carrier of (TopSpaceMetr D)) subsequence of TW

bool the carrier of (TopSpaceMetr D) is non empty set

b . s is Element of bool the carrier of D

rng (TW ^\ s) is Element of bool the carrier of (TopSpaceMetr D)

rngs is Element of bool the carrier of (TopSpaceMetr D)

F is set

dom (TW ^\ s) is V141() V142() V143() V144() V145() V146() Element of bool NAT

F is set

(TW ^\ s) . F is set

R is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

R + s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . (R + s) is Element of bool the carrier of D

X . (R + s) is Element of the carrier of D

f is Element of the carrier of (TopSpaceMetr D)

Lim (TW ^\ s) is Element of bool the carrier of (TopSpaceMetr D)

[:NAT, the carrier of D:] is non empty non trivial non finite set

bool [:NAT, the carrier of D:] is non empty non trivial non finite set

b is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]

the carrier of (TopSpaceMetr D) is non empty set

bool the carrier of (TopSpaceMetr D) is non empty set

X is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,X) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

lim (D,X) is V11() real ext-real Element of REAL

meet X is Element of bool the carrier of D

TW is set

f is Element of the carrier of D

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

S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . rngs is Element of the carrier of D

dist ((b . rngs),f) is V11() real ext-real Element of REAL

the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]

[: the carrier of D, the carrier of D:] is non empty set

[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set

the distance of D . ((b . rngs),f) is V11() real ext-real Element of REAL

(D,X) . rngs is V11() real ext-real Element of REAL

((D,X) . rngs) - 0 is V11() real ext-real Element of REAL

abs (((D,X) . rngs) - 0) is V11() real ext-real Element of REAL

X . rngs is Element of bool the carrier of D

diameter (X . rngs) is V11() real ext-real Element of REAL

{ (b . b

F is Element of bool the carrier of (TopSpaceMetr D)

Cl F is closed Element of bool the carrier of (TopSpaceMetr D)

b . rngs is Element of the carrier of D

dist ((b . rngs),f) is V11() real ext-real Element of REAL

the distance of D . ((b . rngs),f) is V11() real ext-real Element of REAL

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

rng a is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

b is Element of bool (bool the carrier of D)

X is set

W is set

dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is set

a . TW is set

[:X,NAT:] is set

bool [:X,NAT:] is non empty set

W is Relation-like X -defined NAT -valued Function-like total V27(X, NAT ) Element of bool [:X,NAT:]

rng W is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is ordinal natural V11() real finite cardinal ext-real non negative set

dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT

a . TW is Element of bool the carrier of D

f is set

dom W is Element of bool X

bool X is non empty set

s is set

W . s is set

S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

a . S is Element of bool the carrier of D

meet X is set

D is non empty MetrStruct

the carrier of D is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

TopSpaceMetr D is non empty strict TopSpace-like TopStruct

Family_open_set D is Element of bool (bool the carrier of D)

TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr D) is non empty set

bool the carrier of (TopSpaceMetr D) is non empty set

bool (bool the carrier of (TopSpaceMetr D)) is non empty set

a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

rng a is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

X is Element of bool (bool the carrier of (TopSpaceMetr D))

W is Element of bool the carrier of (TopSpaceMetr D)

dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is set

a . TW is set

f is ordinal natural V11() real finite cardinal ext-real non negative set

a . f is Element of bool the carrier of D

W is Element of bool the carrier of (TopSpaceMetr D)

dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is set

a . TW is set

f is ordinal natural V11() real finite cardinal ext-real non negative set

a . f is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

bool the carrier of D is non empty Element of bool (bool the carrier of D)

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

a is Element of bool (bool the carrier of D)

b is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

rng b is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

X is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

W is set

dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . TW is Element of bool the carrier of D

X is set

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

f is Element of bool (bool the carrier of D)

meet f is Element of bool the carrier of D

s is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

meet { (b . b

X is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

W + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

s is set

S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . S is Element of bool the carrier of D

meet { (b . b

X . W is Element of bool the carrier of D

b . 0 is Element of bool the carrier of D

meet { (b . b

X . (W + 1) is Element of bool the carrier of D

W is ordinal natural V11() real finite cardinal ext-real non negative set

{ (b . b

W + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ H

f is set

s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

b . s is Element of bool the carrier of D

W is set

dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT

TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (b . b

meet { (b . b

X . W is set

W is ordinal natural V11() real finite cardinal ext-real non negative set

X . W is Element of bool the carrier of D

{ (b . b

f is Element of bool (bool the carrier of D)

meet f is Element of bool the carrier of D

W is ordinal natural V11() real finite cardinal ext-real non negative set

X . W is Element of bool the carrier of D

{ (b . b

f is Element of bool (bool the carrier of D)

meet f is Element of bool the carrier of D

W is ordinal natural V11() real finite cardinal ext-real non negative set

X . W is Element of bool the carrier of D

{ (b . b

meet { (b . b

D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of D is non empty set

Family_open_set D is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

bool (bool the carrier of D) is non empty set

TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr D) is non empty set

bool the carrier of (TopSpaceMetr D) is non empty set

bool (bool the carrier of (TopSpaceMetr D)) is non empty set

X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

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

b (#) X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

TW is Element of bool (bool the carrier of (TopSpaceMetr D))

meet TW is Element of bool the carrier of (TopSpaceMetr D)

f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

X . f is V11() real ext-real Element of REAL

f + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

1 / (f + 1) is V11() real ext-real non negative Element of REAL

bool the carrier of D is non empty Element of bool (bool the carrier of D)

f is set

s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

s + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

1 / (s + 1) is V11() real ext-real non negative Element of REAL

S is Element of bool the carrier of D

diameter S is V11() real ext-real Element of REAL

rngs is ordinal natural V11() real finite cardinal ext-real non negative set

F is Element of bool the carrier of D

rngs + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

1 / (rngs + 1) is V11() real ext-real non negative Element of REAL

diameter F is V11() real ext-real Element of REAL

[:NAT,(bool the carrier of D):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set

f is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

rng f is Element of bool (bool the carrier of D)

bool (bool the carrier of D) is non empty set

s is set

dom f is V141() V142() V143() V144() V145() V146() Element of bool NAT

S is set

f . S is set

rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

f . rngs is Element of bool the carrier of D

bool the carrier of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))

[:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set

bool [:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set

s is non empty Relation-like NAT -defined bool the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr D)) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr D)):]

f . 0 is Element of bool the carrier of D

rngs is ordinal natural V11() real finite cardinal ext-real non negative set

{ (f . b

meet { (f . b

s . rngs is Element of bool the carrier of (TopSpaceMetr D)

S is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]

S . rngs is Element of bool the carrier of D

rngs is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]

(D,rngs) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]

F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (f . b

f . F is Element of bool the carrier of D

s . F is Element of bool the carrier of (TopSpaceMetr D)

meet { (f . b

rngs . F is Element of bool the carrier of D

diameter (rngs . F) is V11() real ext-real Element of REAL

diameter (f . F) is V11() real ext-real Element of REAL

1 + F is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

1 / (1 + F) is V11() real ext-real non negative Element of REAL

(b (#) X) . F is V11() real ext-real Element of REAL

X . F is V11() real ext-real Element of REAL

b * (X . F) is V11() real ext-real Element of REAL

(D,rngs) . F is V11() real ext-real Element of REAL

lim X is V11() real ext-real Element of REAL

lim (b (#) X) is V11() real ext-real Element of REAL

b * 0 is V11() real ext-real Element of REAL

lim (D,rngs) is V11() real ext-real Element of REAL

meet rngs is Element of bool the carrier of D

F is set

R9 is set

R9 is Element of bool the carrier of (TopSpaceMetr D)

c

SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

s . SI is Element of bool the carrier of (TopSpaceMetr D)

(s . SI) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)

x is ordinal natural V11() real finite cardinal ext-real non negative set

s . x is Element of bool the carrier of (TopSpaceMetr D)

(s . x) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)

c

SI is set

dom c

x is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT

{ (f . b