:: PCOMPS_2 semantic presentation

REAL is V46() V47() V48() V52() set

NAT is non empty V27() V28() V29() V46() V47() V48() V49() V50() V51() V52() Element of bool REAL

bool REAL is non empty set

COMPLEX is V46() V52() set

NAT is non empty V27() V28() V29() V46() V47() V48() V49() V50() V51() V52() set

bool NAT is non empty set

bool NAT is non empty set

1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

[:1,1:] is non empty set

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

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

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

[:[:1,1:],REAL:] is set

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

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

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

2 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is set

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

{} is set

the empty functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered set is empty functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered set

3 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

0 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PT is Relation-like set

metr is set

PT |_2 metr is Relation-like set

[:metr,metr:] is set

PT /\ [:metr,metr:] is set

field (PT |_2 metr) is set

FX is set

[FX,FX] is set

{FX,FX} is finite set

{FX} is finite set

{{FX,FX},{FX}} is finite V59() set

FX is set

R is set

[FX,R] is set

{FX,R} is finite set

{FX} is finite set

{{FX,R},{FX}} is finite V59() set

[R,FX] is set

{R,FX} is finite set

{R} is finite set

{{R,FX},{R}} is finite V59() set

FX is set

R is set

[FX,R] is set

{FX,R} is finite set

{FX} is finite set

{{FX,R},{FX}} is finite V59() set

[R,FX] is set

{R,FX} is finite set

{R} is finite set

{{R,FX},{R}} is finite V59() set

FX is set

R is set

PT -Seg R is set

Coim (PT,R) is set

{R} is finite set

(Coim (PT,R)) \ {R} is Element of bool (Coim (PT,R))

bool (Coim (PT,R)) is non empty set

(PT |_2 metr) -Seg R is set

Coim ((PT |_2 metr),R) is set

(Coim ((PT |_2 metr),R)) \ {R} is Element of bool (Coim ((PT |_2 metr),R))

bool (Coim ((PT |_2 metr),R)) is non empty set

FX is set

[FX,FX] is set

{FX,FX} is finite set

{FX} is finite set

{{FX,FX},{FX}} is finite V59() set

FX is set

R is set

Mn is set

[FX,R] is set

{FX,R} is finite set

{FX} is finite set

{{FX,R},{FX}} is finite V59() set

[R,Mn] is set

{R,Mn} is finite set

{R} is finite set

{{R,Mn},{R}} is finite V59() set

[FX,Mn] is set

{FX,Mn} is finite set

{{FX,Mn},{FX}} is finite V59() set

F

F

PT is set

metr is set

metr is set

metr is set

metr is set

metr is set

FX is set

[metr,FX] is set

{metr,FX} is finite set

{metr} is finite set

{{metr,FX},{metr}} is finite V59() set

PT is set

metr is Relation-like set

FX is Element of PT

metr -Seg FX is set

Coim (metr,FX) is set

{FX} is finite set

(Coim (metr,FX)) \ {FX} is Element of bool (Coim (metr,FX))

bool (Coim (metr,FX)) is non empty set

union (metr -Seg FX) is set

PT is set

metr is Relation-like set

union PT is set

bool (union PT) is non empty Element of bool (bool (union PT))

bool (union PT) is non empty set

bool (bool (union PT)) is non empty set

FX is set

R is set

Mn is set

PM is Element of PT

(PT,metr,PM) is set

metr -Seg PM is set

Coim (metr,PM) is set

{PM} is finite set

(Coim (metr,PM)) \ {PM} is Element of bool (Coim (metr,PM))

bool (Coim (metr,PM)) is non empty set

union (metr -Seg PM) is set

PM \ (PT,metr,PM) is Element of bool PM

bool PM is non empty set

PM is Element of PT

(PT,metr,PM) is set

metr -Seg PM is set

Coim (metr,PM) is set

{PM} is finite set

(Coim (metr,PM)) \ {PM} is Element of bool (Coim (metr,PM))

bool (Coim (metr,PM)) is non empty set

union (metr -Seg PM) is set

PM \ (PT,metr,PM) is Element of bool PM

bool PM is non empty set

PT is set

bool PT is non empty Element of bool (bool PT)

bool PT is non empty set

bool (bool PT) is non empty set

[:NAT,(bool PT):] is non empty set

bool [:NAT,(bool PT):] is non empty set

FX is Relation-like NAT -defined bool PT -valued Function-like V43( NAT , bool PT) Element of bool [:NAT,(bool PT):]

metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

Seg metr is V46() V47() V48() V49() V50() V51() finite V62(metr) Element of bool NAT

{metr} is V46() V47() V48() V49() V50() V51() finite set

(Seg metr) \ {metr} is V46() V47() V48() V49() V50() V51() finite Element of bool NAT

FX .: ((Seg metr) \ {metr}) is finite set

union (FX .: ((Seg metr) \ {metr})) is set

PT is non empty TopSpace-like TopStruct

the carrier of PT is non empty set

bool the carrier of PT is non empty set

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

metr is Element of bool (bool the carrier of PT)

FX is Element of bool (bool the carrier of PT)

R is Element of bool the carrier of PT

Mn is Element of bool the carrier of PT

PM is Element of bool the carrier of PT

Cl Mn is closed Element of bool the carrier of PT

union FX is Element of bool the carrier of PT

R is set

Mn is Element of the carrier of PT

PM is Element of bool the carrier of PT

PM is Element of bool the carrier of PT

PM ` is Element of bool the carrier of PT

(PM `) ` is Element of bool the carrier of PT

UB is Element of bool the carrier of PT

UB is Element of bool the carrier of PT

UB ` is Element of bool the carrier of PT

Cl UB is closed Element of bool the carrier of PT

PM is Element of bool the carrier of PT

PM ` is Element of bool the carrier of PT

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

UB is Element of bool the carrier of PT

{} PT is empty proper functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered open closed Element of bool the carrier of PT

({} PT) ` is open closed Element of bool the carrier of PT

Cl UB is closed Element of bool the carrier of PT

PM is Element of bool the carrier of PT

PM ` is Element of bool the carrier of PT

R is Element of bool the carrier of PT

Cl R is closed Element of bool the carrier of PT

Mn is Element of bool the carrier of PT

PM is Element of bool the carrier of PT

Cl Mn is closed Element of bool the carrier of PT

PT is non empty TopSpace-like TopStruct

the carrier of PT is non empty set

bool the carrier of PT is non empty set

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

metr is Element of bool (bool the carrier of PT)

FX is Element of bool (bool the carrier of PT)

R is Element of bool (bool the carrier of PT)

Mn is Element of bool the carrier of PT

Cl Mn is closed Element of bool the carrier of PT

PM is set

PM is Element of bool the carrier of PT

Cl PM is closed Element of bool the carrier of PT

UB is Element of bool the carrier of PT

clf R is Element of bool (bool the carrier of PT)

Mn is set

PM is Element of bool the carrier of PT

PM is Element of bool the carrier of PT

Cl PM is closed Element of bool the carrier of PT

UB is Element of bool the carrier of PT

PT is non empty TopSpace-like TopStruct

the carrier of PT is non empty set

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

[:[: the carrier of PT, the carrier of PT:],REAL:] is set

bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set

metr is Reflexive discerning symmetric triangle MetrStruct

the carrier of metr is set

FX is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]

SpaceMetr ( the carrier of PT,FX) is strict Reflexive discerning symmetric triangle MetrStruct

MetrStruct(# the carrier of PT,FX #) is strict MetrStruct

PT is non empty TopSpace-like TopStruct

the carrier of PT is non empty set

bool the carrier of PT is non empty set

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

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

[:[: the carrier of PT, the carrier of PT:],REAL:] is set

bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set

R is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]

metr is Reflexive discerning symmetric triangle MetrStruct

SpaceMetr ( the carrier of PT,R) is strict Reflexive discerning symmetric triangle MetrStruct

FX is Element of bool (bool the carrier of PT)

the carrier of metr is set

bool the carrier of metr is non empty set

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

PT is non empty set

bool PT is non empty Element of bool (bool PT)

bool PT is non empty set

bool (bool PT) is non empty set

bool (bool PT) is non empty Element of bool (bool (bool PT))

bool (bool PT) is non empty set

bool (bool (bool PT)) is non empty set

(bool (bool PT)) * is non empty functional FinSequence-membered M10( bool (bool PT))

[:NAT,((bool (bool PT)) *):] is non empty set

bool [:NAT,((bool (bool PT)) *):] is non empty set

metr is Relation-like NAT -defined (bool (bool PT)) * -valued Function-like V43( NAT ,(bool (bool PT)) * ) Element of bool [:NAT,((bool (bool PT)) *):]

FX is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

metr . FX is FinSequence-like set

metr . FX is FinSequence-like Element of (bool (bool PT)) *

F

bool F

bool (bool F

bool F

bool (bool F

bool (bool F

bool (bool (bool F

[:NAT,(bool (bool F

bool [:NAT,(bool (bool F

F

(bool (bool F

<*F

{ (union { F

for b

( not b

<* { (union { F

for b

( not b

metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

FX is Relation-like NAT -defined bool (bool F

{ (union { F

for b

( not b

<* { (union { F

for b

( not b

FX ^ <* { (union { F

for b

( not b

Mn is set

PM is Element of bool F

{ F

for b

( not b

union { F

for b

( not b

PM is set

UB is set

UB is Element of F

F

Mn is Element of bool (bool F

<*Mn*> is non empty Relation-like NAT -defined bool (bool F

PM is Relation-like NAT -defined bool (bool F

FX ^ PM is Relation-like NAT -defined bool (bool F

PM is Relation-like NAT -defined bool (bool F

UB is Relation-like NAT -defined bool (bool F

[:NAT,((bool (bool F

bool [:NAT,((bool (bool F

PT is Relation-like NAT -defined bool (bool F

metr is Relation-like NAT -defined (bool (bool F

(F

FX is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

len (F

FX + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

len (F

(FX + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

{ (union { F

for b

( not b

<* { (union { F

for b

( not b

(F

for b

( not b

len ((F

for b

( not b

(len (F

FX is Relation-like NAT -defined bool (bool F

FX . 0 is Element of bool (bool F

len <*F

<*F

R is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

R + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

FX . (R + 1) is Element of bool (bool F

{ (union { F

for b

( not b

len (F

0 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

len (F

(len (F

(R + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

Mn is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

Mn + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

FX . PM is Element of bool (bool F

PM + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

(F

len (F

(F

Seg (Mn + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62(Mn + 1) Element of bool NAT

len (F

Seg (len (F

dom (F

(Mn + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

Seg ((Mn + 1) + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62((Mn + 1) + 1) Element of bool NAT

len (F

Seg (len (F

dom (F

(F

{ (union { F

for b

( not b

<* { (union { F

for b

( not b

(F

for b

( not b

((F

for b

( not b

(F

(F

{ F

for b

( not b

union { F

for b

( not b

{ F

for b

( not b

union { F

for b

( not b

{ H

(F

len (F

dom (F

Seg ((R + 1) + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62((R + 1) + 1) Element of bool NAT

PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

FX . PM is Element of bool (bool F

PM + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

(F

len (F

(F

PM is Element of bool F

{ F

for b

( not b

union { F

for b

( not b

{ F

for b

( not b

union { F

for b

( not b

PM is Element of F

UB is Element of bool (bool F

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

UB + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

FX . UB is Element of bool (bool F

UB is Element of bool (bool F

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

FX . UB is Element of bool (bool F

UB + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(F

{ H

{ H

{ H

<* { H

(F

len ((F

(F

(F

((F

F

bool F

bool (bool F

bool F

bool (bool F

bool (bool F

bool (bool (bool F

[:NAT,(bool (bool F

bool [:NAT,(bool (bool F

F

PT is Relation-like NAT -defined bool (bool F

PT . 0 is Element of bool (bool F

metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

metr + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PT . (metr + 1) is Element of bool (bool F

{ (union (PT . b

union { (union (PT . b

{ (union { F

{ F

for b

( not b

union { F

for b

( not b

{ F

union { F

{ H

{ H

Mn is Element of bool F

PM is Element of F

PM is set

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PT . UB is Element of bool (bool F

union (PT . UB) is Element of bool F

PM is Element of bool (bool F

union PM is Element of bool F

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PT . UB is Element of bool (bool F

PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PT . PM is Element of bool (bool F

UB is Element of bool (bool F

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

UB is Element of bool (bool F

PT . UB is Element of bool (bool F

union UB is Element of bool F

UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

PM is Element of bool (bool F

PT . UB is Element of bool (bool F

union PM is Element of bool F

f is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

UB is Element of bool (bool F

PT . f is Element of bool (bool F

union UB is Element of bool F

{ H

{ H

{ F

for b

( not b

union { F

for b

( not b

{ F

union { F

PT is non empty TopSpace-like TopStruct

the carrier of PT is non empty set

bool the carrier of PT is non empty set

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

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

[:[: the carrier of PT, the carrier of PT:],REAL:] is set

bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set

the topology of PT is non empty Element of bool (bool the carrier of PT)

metr is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]

SpaceMetr ( the carrier of PT,metr) is strict Reflexive discerning symmetric triangle MetrStruct

Family_open_set (SpaceMetr ( the carrier of PT,metr)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of PT,metr)))

the carrier of (SpaceMetr ( the carrier of PT,metr)) is set

bool the carrier of (SpaceMetr ( the carrier of PT,metr)) is non empty set

bool (bool the carrier of (SpaceMetr ( the carrier of PT,metr))) is non empty set

FX is Element of bool (bool the carrier of PT)

R is Relation-like set

R |_2 FX is Relation-like set

[:FX,FX:] is set

R /\ [:FX,FX:] is set

Mn is Relation-like set

PM is Reflexive discerning symmetric triangle MetrStruct

PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of PM is non empty set

bool the carrier of PM is non empty set

1 / 2 is V34() V35() ext-real Element of REAL

3 / 2 is V34() V35() ext-real Element of REAL

{ (union { (Ball (b

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

UB is set

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

f is set

GX is Element of bool the carrier of PM

((bool the carrier of PM),Mn,GX) is set

Mn -Seg GX is set

Coim (Mn,GX) is set

{GX} is finite set

(Coim (Mn,GX)) \ {GX} is Element of bool (Coim (Mn,GX))

bool (Coim (Mn,GX)) is non empty set

union (Mn -Seg GX) is set

GX \ ((bool the carrier of PM),Mn,GX) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

GX is set

x is set

x9 is Element of the carrier of PM

Ball (x9,(1 / 2)) is Element of bool the carrier of PM

Ball (x9,(3 / 2)) is Element of bool the carrier of PM

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

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

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

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

[:NAT,(bool (bool the carrier of PM)):] is non empty set

bool [:NAT,(bool (bool the carrier of PM)):] is non empty set

UB is Element of bool (bool the carrier of PM)

f is Relation-like NAT -defined bool (bool the carrier of PM) -valued Function-like V43( NAT , bool (bool the carrier of PM)) Element of bool [:NAT,(bool (bool the carrier of PM)):]

f . 0 is Element of bool (bool the carrier of PM)

GX is Element of bool (bool the carrier of PM)

GX is Element of bool (bool the carrier of PT)

x is Element of bool the carrier of PT

x9 is Element of bool the carrier of PM

X is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . X is Element of bool (bool the carrier of PM)

X is Element of bool the carrier of PM

((bool the carrier of PM),Mn,X) is set

Mn -Seg X is set

Coim (Mn,X) is set

{X} is finite set

(Coim (Mn,X)) \ {X} is Element of bool (Coim (Mn,X))

bool (Coim (Mn,X)) is non empty set

union (Mn -Seg X) is set

X \ ((bool the carrier of PM),Mn,X) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

m is set

k is Element of the carrier of PM

Ball (k,(1 / 2)) is Element of bool the carrier of PM

Ball (k,(3 / 2)) is Element of bool the carrier of PM

m is Element of bool (bool the carrier of PM)

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

k is set

W is Element of the carrier of PM

Ball (W,(1 / 2)) is Element of bool the carrier of PM

Ball (W,(3 / 2)) is Element of bool the carrier of PM

X is V27() V28() V29() V33() ext-real non negative set

X + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

r is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

r + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (r + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL

3 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL

{ (union (f . b

union { (union (f . b

{ (union { (Ball (b

m is Element of bool the carrier of PM

((bool the carrier of PM),Mn,m) is set

Mn -Seg m is set

Coim (Mn,m) is set

{m} is finite set

(Coim (Mn,m)) \ {m} is Element of bool (Coim (Mn,m))

bool (Coim (Mn,m)) is non empty set

union (Mn -Seg m) is set

m \ ((bool the carrier of PM),Mn,m) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

k is set

W is set

W is Element of the carrier of PM

Ball (W,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

Ball (W,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

W is Element of bool (bool the carrier of PM)

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

W is set

NZ is Element of the carrier of PM

Ball (NZ,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

Ball (NZ,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

union GX is Element of bool the carrier of PT

x is set

X is Element of bool the carrier of PT

X is set

X is Element of bool the carrier of PT

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

x9 is Element of the carrier of PM

r is Element of bool the carrier of PM

m is V34() V35() ext-real Element of REAL

Ball (x9,m) is Element of bool the carrier of PM

k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ k is V34() V35() ext-real Element of REAL

3 / (2 |^ k) is V34() V35() ext-real Element of REAL

k is V27() V28() V29() V33() ext-real non negative set

2 |^ k is V34() V35() ext-real Element of REAL

3 / (2 |^ k) is V34() V35() ext-real Element of REAL

k + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (k + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(2 |^ k) * 2 is V34() V35() ext-real Element of REAL

3 / (2 |^ (k + 1)) is V34() V35() ext-real Element of REAL

W is set

W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . W is Element of bool (bool the carrier of PM)

W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . W is Element of bool (bool the carrier of PM)

union (f . W) is Element of bool the carrier of PM

W is set

1 / (2 |^ (k + 1)) is V34() V35() ext-real Element of REAL

((bool the carrier of PM),Mn,r) is set

Mn -Seg r is set

Coim (Mn,r) is set

{r} is finite set

(Coim (Mn,r)) \ {r} is Element of bool (Coim (Mn,r))

bool (Coim (Mn,r)) is non empty set

union (Mn -Seg r) is set

r \ ((bool the carrier of PM),Mn,r) is Element of bool the carrier of PM

{ (union (f . b

union { (union (f . b

{ (Ball (b

union { (Ball (b

W is set

NZ is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . NZ is Element of bool (bool the carrier of PM)

union (f . NZ) is Element of bool the carrier of PM

NZ is set

W is set

[NZ,r] is set

{NZ,r} is finite set

{NZ} is finite set

{{NZ,r},{NZ}} is finite V59() set

field Mn is set

[r,NZ] is set

{r,NZ} is finite set

{{r,NZ},{r}} is finite V59() set

Ball (x9,(1 / (2 |^ (k + 1)))) is Element of bool the carrier of PM

W is Element of bool the carrier of PM

Ball (x9,(3 / (2 |^ (k + 1)))) is Element of bool the carrier of PM

W is set

{ (union { (Ball (b

f . (k + 1) is Element of bool (bool the carrier of PM)

W is set

W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . W is Element of bool (bool the carrier of PM)

x is set

x9 is Element of bool the carrier of PM

X is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . X is Element of bool (bool the carrier of PM)

X is Element of bool the carrier of PM

((bool the carrier of PM),Mn,X) is set

Mn -Seg X is set

Coim (Mn,X) is set

{X} is finite set

(Coim (Mn,X)) \ {X} is Element of bool (Coim (Mn,X))

bool (Coim (Mn,X)) is non empty set

union (Mn -Seg X) is set

X \ ((bool the carrier of PM),Mn,X) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

m is set

k is Element of the carrier of PM

Ball (k,(1 / 2)) is Element of bool the carrier of PM

Ball (k,(3 / 2)) is Element of bool the carrier of PM

m is Element of bool (bool the carrier of PM)

k is set

W is Element of the carrier of PM

Ball (W,(1 / 2)) is Element of bool the carrier of PM

Ball (W,(3 / 2)) is Element of bool the carrier of PM

k is set

W is set

X is V27() V28() V29() V33() ext-real non negative set

X + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

r is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

r + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (r + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL

3 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL

{ (union (f . b

union { (union (f . b

{ (union { (Ball (b

m is Element of bool the carrier of PM

((bool the carrier of PM),Mn,m) is set

Mn -Seg m is set

Coim (Mn,m) is set

{m} is finite set

(Coim (Mn,m)) \ {m} is Element of bool (Coim (Mn,m))

bool (Coim (Mn,m)) is non empty set

union (Mn -Seg m) is set

m \ ((bool the carrier of PM),Mn,m) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

k is set

W is set

W is Element of the carrier of PM

Ball (W,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

Ball (W,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

W is Element of bool (bool the carrier of PM)

W is set

NZ is Element of the carrier of PM

Ball (NZ,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

Ball (NZ,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM

W is set

NZ is set

X is set

x is Element of the carrier of PT

X is Element of bool the carrier of PT

X is Element of bool the carrier of PT

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

x9 is Element of the carrier of PM

r is V34() V35() ext-real Element of REAL

Ball (x9,r) is Element of bool the carrier of PM

m is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ m is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ m) is V34() V35() ext-real Element of REAL

k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . k is set

k is V27() V28() V29() V33() ext-real non negative set

f . k is set

m + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(m + 1) + k is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

((m + 1) + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (((m + 1) + k) + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL

Ball (x9,(1 / (2 |^ (((m + 1) + k) + 1)))) is Element of bool the carrier of PM

W is Element of bool the carrier of PM

W is Element of bool the carrier of PT

{ b

g is set

x is Element of bool the carrier of PT

g is Relation-like Function-like set

dom g is set

rng g is set

{ b

x is set

x1 is set

g . x1 is set

n1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . n1 is Element of bool (bool the carrier of PM)

n1 is Element of bool the carrier of PT

w1 is set

w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

w1 is V27() V28() V29() V33() ext-real non negative set

w1 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

w2 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (w2 + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ (w2 + 1)) is V34() V35() ext-real Element of REAL

3 / (2 |^ (w2 + 1)) is V34() V35() ext-real Element of REAL

{ (union (f . b

union { (union (f . b

{ (union { (Ball (b

l is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . l is Element of bool (bool the carrier of PM)

2 |^ w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ w2) is V34() V35() ext-real Element of REAL

l is Element of bool the carrier of PM

((bool the carrier of PM),Mn,l) is set

Mn -Seg l is set

Coim (Mn,l) is set

{l} is finite set

(Coim (Mn,l)) \ {l} is Element of bool (Coim (Mn,l))

bool (Coim (Mn,l)) is non empty set

union (Mn -Seg l) is set

l \ ((bool the carrier of PM),Mn,l) is Element of bool the carrier of PM

{ (Ball (b

union { (Ball (b

l is set

h is set

M1 is Element of the carrier of PM

Ball (M1,(1 / (2 |^ (w2 + 1)))) is Element of bool the carrier of PM

Ball (M1,(3 / (2 |^ (w2 + 1)))) is Element of bool the carrier of PM

i is Element of the carrier of PM

dist (M1,i) is V34() V35() ext-real Element of REAL

dist (i,x9) is V34() V35() ext-real Element of REAL

(1 / (2 |^ (((m + 1) + k) + 1))) + (dist (i,x9)) is V34() V35() ext-real Element of REAL

(dist (M1,i)) + (dist (i,x9)) is V34() V35() ext-real Element of REAL

NF is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . NF is Element of bool (bool the carrier of PM)

union (f . NF) is Element of bool the carrier of PM

dist (M1,x9) is V34() V35() ext-real Element of REAL

dist (x9,M1) is V34() V35() ext-real Element of REAL

f . k is Element of bool (bool the carrier of PM)

union (f . k) is Element of bool the carrier of PM

k + (m + 1) is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

1 + k is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (1 + k) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(2 |^ (1 + k)) * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 - 1 is V34() V35() ext-real Element of REAL

((2 |^ (1 + k)) * 2) - 1 is V34() V35() ext-real Element of REAL

(1 + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ ((1 + k) + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 * (2 |^ ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(2 |^ m) * (2 |^ ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1))) is V34() V35() ext-real Element of REAL

((1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

m + ((1 + k) + 1) is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ (m + ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1))) is V34() V35() ext-real Element of REAL

((1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

((2 |^ (1 + k)) * 2) / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL

(((2 |^ (1 + k)) * 2) / (2 |^ (((m + 1) + k) + 1))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

(((2 |^ (1 + k)) * 2) - 1) / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL

x is set

x1 is set

g . x is set

g . x1 is set

w2 is Element of bool the carrier of PT

w2 is set

n1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

f . n1 is Element of bool (bool the carrier of PM)

w1 is Element of bool the carrier of PT

w1 is set

m + k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(m + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ 1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

2 |^ ((m + 1) + k) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

1 / (2 |^ ((m + 1) + k)) is V34() V35() ext-real Element of REAL

2 / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL

1 * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(2 |^ ((m + 1) + k)) * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(1 * 2) / ((2 |^ ((m + 1) + k)) * 2) is V34() V35() ext-real Element of REAL

(1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2) is V34() V35() ext-real Element of REAL

((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) is V34() V35() ext-real Element of REAL

1 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT

(1 + 1) / 2 is V34() V35() ext-real Element of REAL

(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL

((1 + 1) / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1