:: KURATO_2 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is non empty set

K204() is non empty strict TopSpace-like TopStruct

the carrier of K204() is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

[:1,1:] is non empty Relation-like set

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

[:[:1,1:],1:] is non empty Relation-like set

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

[:[:1,1:],REAL:] is Relation-like set

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

[:REAL,REAL:] is Relation-like set

[:[:REAL,REAL:],REAL:] is Relation-like set

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

[:2,2:] is non empty Relation-like set

[:[:2,2:],REAL:] is Relation-like set

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

bool NAT is non empty set

COMPLEX is set

RAT is set

INT is set

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

K406() is non empty V128() L10()

the carrier of K406() is non empty set

K411() is non empty V128() V150() V151() V152() V154() V204() V205() V206() V207() V208() V209() L10()

K412() is non empty V128() V152() V154() V207() V208() V209() M19(K411())

K413() is non empty V128() V150() V152() V154() V207() V208() V209() V210() M22(K411(),K412())

K415() is non empty V128() V150() V152() V154() L10()

K416() is non empty V128() V150() V152() V154() V210() M19(K415())

TOP-REAL 2 is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL 2) is non empty set

[:NAT,REAL:] is Relation-like set

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

bool the carrier of (TOP-REAL 2) is non empty set

bool (bool REAL) is non empty set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set

0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

[:NAT,NAT:] is non empty Relation-like set

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

F is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)

L~ F is closed boundary nowhere_dense Element of bool the carrier of (TOP-REAL 2)

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty set

G is Element of the carrier of (Euclid F)

i is V11() real ext-real set

Ball (G,i) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

H is Element of bool the carrier of (TOP-REAL F)

NS is Element of bool the carrier of (TOP-REAL F)

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL F) is non empty set

G is Element of the carrier of (Euclid F)

H is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i - H is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

K389(i,H) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

|.(i - H).| is V11() real ext-real non negative Element of REAL

NS is V11() real ext-real set

Ball (G,NS) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is Element of the carrier of (Euclid F)

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL F) is non empty set

G is Element of the carrier of (Euclid F)

H is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i - H is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

K389(i,H) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

|.(i - H).| is V11() real ext-real non negative Element of REAL

NS is V11() real ext-real set

Ball (G,NS) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is Element of the carrier of (Euclid F)

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty set

[:NAT, the carrier of (TOP-REAL F):] is non empty Relation-like set

bool [:NAT, the carrier of (TOP-REAL F):] is non empty set

G is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i is Element of bool the carrier of (TOP-REAL F)

Cl i is closed Element of bool the carrier of (TOP-REAL F)

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

H is Element of the carrier of (Euclid F)

NS is set

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

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

(P + 1) " is non empty V11() real ext-real positive non negative set

1 * ((P + 1) ") is V11() real ext-real non negative set

Ball (H,(1 / (P + 1))) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

i is open Element of bool the carrier of (TOP-REAL F)

i /\ i is Element of bool the carrier of (TOP-REAL F)

choose (i /\ i) is Element of i /\ i

the Element of i /\ i is Element of i /\ i

i is set

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

c

NS is Relation-like Function-like set

proj1 NS is set

proj2 NS is set

P is non empty Relation-like NAT -defined the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , the carrier of (TOP-REAL F)) Element of bool [:NAT, the carrier of (TOP-REAL F):]

rng P is non empty Element of bool the carrier of (TOP-REAL F)

lim P is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

P is set

dom P is non empty Element of bool NAT

P is set

P . P is set

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

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

(i + 1) " is non empty V11() real ext-real positive non negative set

1 * ((i + 1) ") is V11() real ext-real non negative set

Ball (H,(1 / (i + 1))) is Element of bool the carrier of (Euclid F)

i /\ (Ball (H,(1 / (i + 1)))) is Element of bool the carrier of (Euclid F)

choose (i /\ (Ball (H,(1 / (i + 1))))) is Element of i /\ (Ball (H,(1 / (i + 1))))

the Element of i /\ (Ball (H,(1 / (i + 1)))) is Element of i /\ (Ball (H,(1 / (i + 1))))

c

i /\ c

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

1 / P is V11() real ext-real Element of REAL

P " is V11() real ext-real set

1 * (P ") is V11() real ext-real set

[/(1 / P)\] is V11() real integer ext-real set

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

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

i " is V11() real ext-real non negative set

1 * (i ") is V11() real ext-real non negative set

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

(i + 1) " is non empty V11() real ext-real positive non negative set

1 * ((i + 1) ") is V11() real ext-real non negative set

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

i " is V11() real ext-real non negative set

1 * (i ") is V11() real ext-real non negative set

1 / (1 / P) is V11() real ext-real Element of REAL

(1 / P) " is V11() real ext-real set

1 * ((1 / P) ") is V11() real ext-real set

c

c

1 / (c

(c

1 * ((c

Ball (H,(1 / (c

k2 is open Element of bool the carrier of (TOP-REAL F)

i /\ k2 is Element of bool the carrier of (TOP-REAL F)

P . c

k1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

k1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

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

(k1 + 1) " is non empty V11() real ext-real positive non negative set

1 * ((k1 + 1) ") is V11() real ext-real non negative set

Ball (H,(1 / (k1 + 1))) is Element of bool the carrier of (Euclid F)

i /\ (Ball (H,(1 / (k1 + 1)))) is Element of bool the carrier of (Euclid F)

choose (i /\ (Ball (H,(1 / (k1 + 1))))) is Element of i /\ (Ball (H,(1 / (k1 + 1))))

the Element of i /\ (Ball (H,(1 / (k1 + 1)))) is Element of i /\ (Ball (H,(1 / (k1 + 1))))

(P . c

K389((P . c

|.((P . c

F is non empty Reflexive discerning V98() triangle Discerning MetrStruct

TopSpaceMetr F is non empty strict TopSpace-like TopStruct

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

TopStruct(# the carrier of F, the topology of F #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

bool the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #)) is non empty set

G is Element of the carrier of F

i is Element of the carrier of TopStruct(# the carrier of F, the topology of F #)

H is set

NS is Element of bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #))

the topology of TopStruct(# the carrier of F, the topology of F #) is non empty Element of bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #))

Intersect NS is Element of bool the carrier of TopStruct(# the carrier of F, the topology of F #)

P is Element of bool the carrier of TopStruct(# the carrier of F, the topology of F #)

P is Element of bool the carrier of F

P is Element of bool the carrier of F

i is Element of bool the carrier of TopStruct(# the carrier of F, the topology of F #)

NS is Element of bool (bool the carrier of F)

Intersect NS is Element of bool the carrier of F

P is Element of bool the carrier of F

P is Element of bool the carrier of TopStruct(# the carrier of F, the topology of F #)

P is Element of bool the carrier of TopStruct(# the carrier of F, the topology of F #)

i is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

TopStruct(# the carrier of F, the topology of F #) is non empty strict TopSpace-like TopStruct

the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

G is Element of the carrier of TopStruct(# the carrier of F, the topology of F #)

bool the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #)) is non empty set

i is Element of the carrier of F

H is i -quasi_basis open Element of bool (bool the carrier of F)

NS is G -quasi_basis open Element of bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #))

G is Element of the carrier of F

the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

i is Element of the carrier of TopStruct(# the carrier of F, the topology of F #)

bool the carrier of TopStruct(# the carrier of F, the topology of F #) is non empty set

bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #)) is non empty set

H is i -quasi_basis open Element of bool (bool the carrier of TopStruct(# the carrier of F, the topology of F #))

NS is G -quasi_basis open Element of bool (bool the carrier of F)

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() L16()

the carrier of (TOP-REAL F) is non empty set

the topology of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool the carrier of (TOP-REAL F) is non empty set

bool (bool the carrier of (TOP-REAL F)) is non empty set

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

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

TopSpaceMetr (Euclid F) is non empty strict TopSpace-like first-countable TopStruct

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty set

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is Element of bool the carrier of (TOP-REAL F)

Cl G is closed Element of bool the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

H is Element of the carrier of (Euclid F)

NS is V11() real ext-real set

Ball (H,NS) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is Element of bool the carrier of (TOP-REAL F)

NS is a_neighborhood of i

Int NS is open Element of bool the carrier of (TOP-REAL F)

P is V11() real ext-real set

Ball (H,P) is Element of bool the carrier of (Euclid F)

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

H is Element of the carrier of (Euclid F)

NS is Element of the carrier of (Euclid F)

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

(dist (H,NS)) / 2 is V11() real ext-real Element of REAL

2 " is non empty V11() real ext-real positive non negative set

(dist (H,NS)) * (2 ") is V11() real ext-real set

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

Ball (H,P) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty set

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is Element of bool the carrier of (TOP-REAL F)

bool the carrier of (Euclid F) is non empty set

i is Element of bool the carrier of (Euclid F)

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

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is V11() real ext-real set

i is V11() real ext-real set

G + i is V11() real ext-real set

H is Element of the carrier of (Euclid F)

Ball (H,G) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

NS is Element of the carrier of (Euclid F)

Ball (NS,i) is Element of bool the carrier of (Euclid F)

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

P is set

P is Element of the carrier of (Euclid F)

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

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

(dist (H,P)) + i is V11() real ext-real Element of REAL

(dist (H,P)) + (dist (NS,P)) is V11() real ext-real Element of REAL

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is V11() real ext-real set

H is V11() real ext-real set

i is V11() real ext-real set

G + i is V11() real ext-real set

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

(G + i) + (2 * H) is V11() real ext-real Element of REAL

NS is Element of the carrier of (Euclid F)

Ball (NS,G) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is Element of the carrier of (Euclid F)

Ball (P,H) is Element of bool the carrier of (Euclid F)

P is Element of the carrier of (Euclid F)

Ball (P,i) is Element of bool the carrier of (Euclid F)

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

G + H is V11() real ext-real set

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

(G + H) + (dist (P,P)) is V11() real ext-real Element of REAL

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

(dist (NS,P)) + (dist (P,P)) is V11() real ext-real Element of REAL

H + i is V11() real ext-real set

(G + H) + (H + i) is V11() real ext-real set

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

[:F,G:] is non empty strict TopSpace-like TopStruct

the carrier of [:F,G:] is non empty set

bool the carrier of [:F,G:] is non empty set

i is Element of the carrier of F

{i} is compact Element of bool the carrier of F

bool the carrier of F is non empty set

H is Element of the carrier of G

{H} is compact Element of bool the carrier of G

bool the carrier of G is non empty set

[:{i},{H}:] is Relation-like Element of bool the carrier of [:F,G:]

[i,H] is V24() Element of the carrier of [:F,G:]

{i,H} is set

{i} is set

{{i,H},{i}} is set

NS is Element of bool the carrier of [:F,G:]

{[i,H]} is Relation-like compact Element of bool the carrier of [:F,G:]

F is non empty 1-sorted

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

H is Element of bool the carrier of F

NS is non empty Relation-like NAT -defined NAT -valued Function-like V23( NAT ) V27( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

G * NS is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . P is Element of bool the carrier of F

G . P is Element of bool the carrier of F

dom NS is non empty Element of bool NAT

NS . P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . (NS . P) is Element of bool the carrier of F

dom G is non empty Element of bool NAT

P is set

G . P is set

i . P is set

dom i is non empty Element of bool NAT

F is non empty 1-sorted

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

H is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . H is Element of bool the carrier of F

NS is non empty Relation-like NAT -defined NAT -valued Function-like V23( NAT ) V27( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

G * NS is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

NS . H is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . P is Element of bool the carrier of F

dom NS is non empty Element of bool NAT

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is Element of bool the carrier of F

H is Element of bool the carrier of F

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool the carrier of (TOP-REAL F) is non empty set

bool (bool the carrier of (TOP-REAL F)) is non empty set

[:NAT,(bool the carrier of (TOP-REAL F)):] is non empty Relation-like set

bool [:NAT,(bool the carrier of (TOP-REAL F)):] is non empty set

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL F)) Element of bool [:NAT,(bool the carrier of (TOP-REAL F)):]

((TOP-REAL F),G) is Element of bool the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

H is Element of the carrier of (Euclid F)

NS is V11() real ext-real set

Ball (H,NS) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is a_neighborhood of i

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

the topology of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

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

TopSpaceMetr (Euclid F) is non empty strict TopSpace-like first-countable TopStruct

the carrier of (TopSpaceMetr (Euclid F)) is non empty set

bool the carrier of (TopSpaceMetr (Euclid F)) is non empty set

NS is a_neighborhood of i

Int NS is open Element of bool the carrier of (TOP-REAL F)

P is Element of bool the carrier of (TopSpaceMetr (Euclid F))

P is V11() real ext-real set

Ball (H,P) is Element of bool the carrier of (Euclid F)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Element of bool the carrier of (TOP-REAL F)

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is Element of bool the carrier of F

Cl (F,G) is closed Element of bool the carrier of F

i is set

H is Element of the carrier of F

NS is a_neighborhood of H

Int NS is open Element of bool the carrier of F

P is set

P is Element of the carrier of F

Int (Int NS) is open Element of bool the carrier of F

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

c

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . c

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is Element of bool the carrier of F

Cl (F,G) is closed Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,i) is closed Element of bool the carrier of F

(F,G) is closed Element of bool the carrier of F

H is non empty Relation-like NAT -defined NAT -valued Function-like V23( NAT ) V27( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

i * H is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of i

NS is set

P is Element of the carrier of F

P is a_neighborhood of P

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Element of bool the carrier of F

H . i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

dom H is non empty Element of bool NAT

i . (H . i) is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is closed Element of bool the carrier of F

(F,i) is closed Element of bool the carrier of F

H is set

NS is Element of the carrier of F

P is a_neighborhood of NS

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . P is Element of bool the carrier of F

G . P is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

H is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is closed Element of bool the carrier of F

(F,i) is closed Element of bool the carrier of F

(F,G) \/ (F,i) is closed Element of bool the carrier of F

(F,H) is closed Element of bool the carrier of F

NS is set

P is Element of the carrier of F

P is a_neighborhood of P

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

H . i is Element of bool the carrier of F

G . i is Element of bool the carrier of F

i . i is Element of bool the carrier of F

(G . i) \/ (i . i) is Element of bool the carrier of F

P is Element of the carrier of F

P is a_neighborhood of P

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

H . i is Element of bool the carrier of F

i . i is Element of bool the carrier of F

G . i is Element of bool the carrier of F

(G . i) \/ (i . i) is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

H is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,H) is closed Element of bool the carrier of F

(F,G) is closed Element of bool the carrier of F

(F,i) is closed Element of bool the carrier of F

(F,G) /\ (F,i) is closed Element of bool the carrier of F

NS is set

P is Element of the carrier of F

P is a_neighborhood of P

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . i is Element of bool the carrier of F

H . i is Element of bool the carrier of F

G . i is Element of bool the carrier of F

(G . i) /\ (i . i) is Element of bool the carrier of F

P is a_neighborhood of P

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Element of bool the carrier of F

H . i is Element of bool the carrier of F

i . i is Element of bool the carrier of F

(G . i) /\ (i . i) is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,i) is closed Element of bool the carrier of F

(F,G) is closed Element of bool the carrier of F

H is set

NS is Element of the carrier of F

P is a_neighborhood of NS

P is non empty Element of bool the carrier of F

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Element of bool the carrier of F

i . i is Element of bool the carrier of F

i is set

c

m is non empty Element of bool the carrier of F

Cl (G . i) is closed Element of bool the carrier of F

H is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . H is Element of bool the carrier of F

i . H is Element of bool the carrier of F

Cl (G . H) is closed Element of bool the carrier of F

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool the carrier of (TOP-REAL F) is non empty set

bool (bool the carrier of (TOP-REAL F)) is non empty set

[:NAT,(bool the carrier of (TOP-REAL F)):] is non empty Relation-like set

bool [:NAT,(bool the carrier of (TOP-REAL F)):] is non empty set

[:NAT, the carrier of (TOP-REAL F):] is non empty Relation-like set

bool [:NAT, the carrier of (TOP-REAL F):] is non empty set

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL F)) Element of bool [:NAT,(bool the carrier of (TOP-REAL F)):]

((TOP-REAL F),G) is closed Element of bool the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

NS is non empty Relation-like NAT -defined the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , the carrier of (TOP-REAL F)) Element of bool [:NAT, the carrier of (TOP-REAL F):]

lim NS is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

H is Element of the carrier of (Euclid F)

P is V11() real ext-real set

Ball (H,P) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

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

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

max (0,P) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Element of bool the carrier of (TOP-REAL F)

NS . i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

(NS . i) - i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

K389((NS . i),i) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

|.((NS . i) - i).| is V11() real ext-real non negative Element of REAL

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

bool the carrier of F is non empty set

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

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is Element of bool the carrier of F

Cl G is closed Element of bool the carrier of F

i is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,i) is closed Element of bool the carrier of F

H is set

NS is Element of the carrier of F

P is Element of bool the carrier of F

P is a_neighborhood of NS

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

i . (P + 1) is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is closed Element of bool the carrier of F

i is Element of bool the carrier of F

Cl i is closed Element of bool the carrier of F

H is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set

G . H is set

H is set

NS is Element of the carrier of F

P is a_neighborhood of NS

P is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . P is Element of bool the carrier of F

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is closed Element of bool the carrier of F

i is closed Element of bool the carrier of F

Cl i is closed Element of bool the carrier of F

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool the carrier of (TOP-REAL F) is non empty set

bool (bool the carrier of (TOP-REAL F)) is non empty set

[:NAT,(bool the carrier of (TOP-REAL F)):] is non empty Relation-like set

bool [:NAT,(bool the carrier of (TOP-REAL F)):] is non empty set

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL F)) Element of bool [:NAT,(bool the carrier of (TOP-REAL F)):]

((TOP-REAL F),G) is closed Element of bool the carrier of (TOP-REAL F)

i is Element of bool the carrier of (TOP-REAL F)

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

bool the carrier of (Euclid F) is non empty set

H is bounded Element of bool the carrier of (Euclid F)

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

P is Element of the carrier of (Euclid F)

Ball (P,NS) is Element of bool the carrier of (Euclid F)

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT

3 * NS is V11() real ext-real Element of REAL

(1 + 1) + (3 * NS) is V11() real ext-real Element of REAL

i is Element of the carrier of (Euclid F)

i is Element of the carrier of (Euclid F)

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

Ball (i,1) is Element of bool the carrier of (Euclid F)

c

Ball (i,1) is Element of bool the carrier of (Euclid F)

m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

max (c

(max (c

G . ((max (c

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

(1 + 1) + (2 * NS) is V11() real ext-real Element of REAL

bool the carrier of (TOP-REAL 2) is non empty Element of bool (bool the carrier of (TOP-REAL 2))

bool (bool the carrier of (TOP-REAL 2)) is non empty set

[:NAT,(bool the carrier of (TOP-REAL 2)):] is non empty Relation-like set

bool [:NAT,(bool the carrier of (TOP-REAL 2)):] is non empty set

G is Element of bool the carrier of (TOP-REAL 2)

F is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

((TOP-REAL 2),F) is closed Element of bool the carrier of (TOP-REAL 2)

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

bool the carrier of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool the carrier of (TOP-REAL F) is non empty set

bool (bool the carrier of (TOP-REAL F)) is non empty set

[:NAT,(bool the carrier of (TOP-REAL F)):] is non empty Relation-like set

bool [:NAT,(bool the carrier of (TOP-REAL F)):] is non empty set

[:(TOP-REAL F),(TOP-REAL F):] is non empty strict TopSpace-like TopStruct

the carrier of [:(TOP-REAL F),(TOP-REAL F):] is non empty set

bool the carrier of [:(TOP-REAL F),(TOP-REAL F):] is non empty Element of bool (bool the carrier of [:(TOP-REAL F),(TOP-REAL F):])

bool the carrier of [:(TOP-REAL F),(TOP-REAL F):] is non empty set

bool (bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]) is non empty set

[:NAT,(bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]):] is non empty Relation-like set

bool [:NAT,(bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]):] is non empty set

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL F)) Element of bool [:NAT,(bool the carrier of (TOP-REAL F)):]

i is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL F)) Element of bool [:NAT,(bool the carrier of (TOP-REAL F)):]

((TOP-REAL F),G) is closed Element of bool the carrier of (TOP-REAL F)

((TOP-REAL F),i) is closed Element of bool the carrier of (TOP-REAL F)

[:((TOP-REAL F),G),((TOP-REAL F),i):] is Relation-like Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

H is non empty Relation-like NAT -defined bool the carrier of [:(TOP-REAL F),(TOP-REAL F):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]) Element of bool [:NAT,(bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]):]

([:(TOP-REAL F),(TOP-REAL F):],H) is closed Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

NS is set

P is set

P is set

[P,P] is V24() set

{P,P} is set

{P} is set

{{P,P},{P}} is set

P is Element of the carrier of [:(TOP-REAL F),(TOP-REAL F):]

c

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

{i} is bounded compact Element of bool the carrier of (TOP-REAL F)

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

{i} is bounded compact Element of bool the carrier of (TOP-REAL F)

[:{i},{i}:] is Relation-like Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

m is a_neighborhood of {i}

y is a_neighborhood of i

[:m,y:] is Relation-like a_neighborhood of [:{i},{i}:]

k2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

k1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

max (k1,k2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

H . m is Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

i . m is Element of bool the carrier of (TOP-REAL F)

G . m is Element of bool the carrier of (TOP-REAL F)

[:(G . m),(i . m):] is Relation-like Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

NS is set

[: the carrier of (TOP-REAL F), the carrier of (TOP-REAL F):] is non empty Relation-like set

NS `1 is set

NS `2 is set

P is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

the a_neighborhood of P is a_neighborhood of P

P is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

the a_neighborhood of P is a_neighborhood of P

[P,P] is V24() Element of the carrier of [:(TOP-REAL F),(TOP-REAL F):]

{P,P} is set

{P} is set

{{P,P},{P}} is set

i is a_neighborhood of P

[: the a_neighborhood of P,i:] is Relation-like a_neighborhood of [P,P]

c

m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . m is Element of bool the carrier of (TOP-REAL F)

H . m is Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

y is set

G . m is Element of bool the carrier of (TOP-REAL F)

[:(G . m),(i . m):] is Relation-like Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

y `2 is set

i is a_neighborhood of P

[:i, the a_neighborhood of P:] is Relation-like a_neighborhood of [P,P]

c

m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . m is Element of bool the carrier of (TOP-REAL F)

H . m is Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

y is set

i . m is Element of bool the carrier of (TOP-REAL F)

[:(G . m),(i . m):] is Relation-like Element of bool the carrier of [:(TOP-REAL F),(TOP-REAL F):]

y `1 is set

F is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

lim_inf F is Element of bool the carrier of (TOP-REAL 2)

((TOP-REAL 2),F) is closed Element of bool the carrier of (TOP-REAL 2)

G is set

Euclid 2 is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid 2) is non empty set

NS is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is Element of the carrier of (Euclid 2)

P is V11() real ext-real set

Ball (i,P) is Element of bool the carrier of (Euclid 2)

bool the carrier of (Euclid 2) is non empty set

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

F . P is Element of bool the carrier of (TOP-REAL 2)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set

NS + P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

H is Relation-like Function-like V37(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)

F is non empty bounded being_simple_closed_curve compact V256() V257() Element of bool the carrier of (TOP-REAL 2)

G is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

Cage (F,G) is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant FinSequence-like V235( the carrier of (TOP-REAL 2)) special unfolded V241() V242() V259() FinSequence of the carrier of (TOP-REAL 2)

L~ (Cage (F,G)) is closed boundary nowhere_dense Element of bool the carrier of (TOP-REAL 2)

UBD (L~ (Cage (F,G))) is open Element of bool the carrier of (TOP-REAL 2)

(UBD (L~ (Cage (F,G)))) ` is closed Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ (UBD (L~ (Cage (F,G)))) is set

Fr ((UBD (L~ (Cage (F,G)))) `) is closed boundary nowhere_dense Element of bool the carrier of (TOP-REAL 2)

BDD (L~ (Cage (F,G))) is open Element of bool the carrier of (TOP-REAL 2)

(BDD (L~ (Cage (F,G)))) ` is closed Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ (BDD (L~ (Cage (F,G)))) is set

(BDD (L~ (Cage (F,G)))) \/ ((BDD (L~ (Cage (F,G)))) `) is Element of bool the carrier of (TOP-REAL 2)

[#] (TOP-REAL 2) is non empty non proper open closed dense non boundary Element of bool the carrier of (TOP-REAL 2)

(L~ (Cage (F,G))) ` is open dense Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ (L~ (Cage (F,G))) is set

(BDD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G))) is Element of bool the carrier of (TOP-REAL 2)

((L~ (Cage (F,G))) `) \/ (L~ (Cage (F,G))) is Element of bool the carrier of (TOP-REAL 2)

(BDD (L~ (Cage (F,G)))) \/ (UBD (L~ (Cage (F,G)))) is open Element of bool the carrier of (TOP-REAL 2)

((BDD (L~ (Cage (F,G)))) \/ (UBD (L~ (Cage (F,G))))) \/ (L~ (Cage (F,G))) is Element of bool the carrier of (TOP-REAL 2)

(UBD (L~ (Cage (F,G)))) \/ ((BDD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G)))) is Element of bool the carrier of (TOP-REAL 2)

((UBD (L~ (Cage (F,G)))) \/ ((BDD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G))))) \ (UBD (L~ (Cage (F,G)))) is Element of bool the carrier of (TOP-REAL 2)

(L~ (Cage (F,G))) \/ (BDD (L~ (Cage (F,G)))) is Element of bool the carrier of (TOP-REAL 2)

((BDD (L~ (Cage (F,G)))) \/ (UBD (L~ (Cage (F,G))))) ` is closed Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ ((BDD (L~ (Cage (F,G)))) \/ (UBD (L~ (Cage (F,G))))) is set

((L~ (Cage (F,G))) `) ` is closed Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ ((L~ (Cage (F,G))) `) is set

((BDD (L~ (Cage (F,G)))) `) /\ ((UBD (L~ (Cage (F,G)))) `) is closed Element of bool the carrier of (TOP-REAL 2)

(BDD (L~ (Cage (F,G)))) \/ ((UBD (L~ (Cage (F,G)))) `) is Element of bool the carrier of (TOP-REAL 2)

((BDD (L~ (Cage (F,G)))) \/ ((BDD (L~ (Cage (F,G)))) `)) /\ ((BDD (L~ (Cage (F,G)))) \/ ((UBD (L~ (Cage (F,G)))) `)) is Element of bool the carrier of (TOP-REAL 2)

Cl ((UBD (L~ (Cage (F,G)))) `) is closed Element of bool the carrier of (TOP-REAL 2)

((UBD (L~ (Cage (F,G)))) `) ` is open Element of bool the carrier of (TOP-REAL 2)

the carrier of (TOP-REAL 2) \ ((UBD (L~ (Cage (F,G)))) `) is set

LeftComp (Cage (F,G)) is Element of bool the carrier of (TOP-REAL 2)

(BDD (L~ (Cage (F,G)))) /\ (UBD (L~ (Cage (F,G)))) is open Element of bool the carrier of (TOP-REAL 2)

Cl (((UBD (L~ (Cage (F,G)))) `) `) is closed Element of bool the carrier of (TOP-REAL 2)

(Cl ((UBD (L~ (Cage (F,G)))) `)) /\ (Cl (((UBD (L~ (Cage (F,G)))) `) `)) is closed Element of bool the carrier of (TOP-REAL 2)

(UBD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G))) is Element of bool the carrier of (TOP-REAL 2)

((BDD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G)))) /\ ((UBD (L~ (Cage (F,G)))) \/ (L~ (Cage (F,G)))) is Element of bool the carrier of (TOP-REAL 2)

((BDD (L~ (Cage (F,G)))) /\ (UBD (L~ (Cage (F,G))))) \/ (L~ (Cage (F,G))) is Element of bool the carrier of (TOP-REAL 2)

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

i is set

H is set

H is Element of bool the carrier of F

NS is set

P is set

P is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

(F,P) is closed Element of bool the carrier of F

i is Element of bool the carrier of F

H is Element of bool the carrier of F

F is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

TOP-REAL F is non empty TopSpace-like V126() V194() V195() V212() V213() V214() V215() V216() V217() V218() strict V225() V226() first-countable L16()

the carrier of (TOP-REAL F) is non empty set

[:NAT, the carrier of (TOP-REAL F):] is non empty Relation-like set

bool [:NAT, the carrier of (TOP-REAL F):] is non empty set

Euclid F is non empty strict Reflexive discerning V98() triangle Discerning MetrStruct

the carrier of (Euclid F) is non empty set

G is non empty Relation-like NAT -defined the carrier of (TOP-REAL F) -valued Function-like V23( NAT ) V27( NAT , the carrier of (TOP-REAL F)) Element of bool [:NAT, the carrier of (TOP-REAL F):]

i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

H is Element of the carrier of (Euclid F)

bool the carrier of (TOP-REAL F) is non empty set

NS is V11() real ext-real set

Ball (H,NS) is Element of bool the carrier of (Euclid F)

bool the carrier of (Euclid F) is non empty set

P is open Element of bool the carrier of (TOP-REAL F)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . P is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

NS is Element of bool the carrier of (TOP-REAL F)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

the topology of (TOP-REAL F) is non empty Element of bool (bool the carrier of (TOP-REAL F))

bool (bool the carrier of (TOP-REAL F)) is non empty set

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

TopSpaceMetr (Euclid F) is non empty strict TopSpace-like first-countable TopStruct

the carrier of (TopSpaceMetr (Euclid F)) is non empty set

bool the carrier of (TopSpaceMetr (Euclid F)) is non empty set

P is Element of bool the carrier of (TopSpaceMetr (Euclid F))

i is V11() real ext-real set

Ball (H,i) is Element of bool the carrier of (Euclid F)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

G . i is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

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

bool the carrier of F is non empty set

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

[:NAT,(bool the carrier of F):] is non empty Relation-like set

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

G is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) Element of bool [:NAT,(bool the carrier of F):]

(F,G) is closed Element of bool the carrier of F

(F,G) is Element of bool the carrier of F

i is set

H is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

(F,H) is closed Element of bool the carrier of F

H is non empty Relation-like NAT -defined bool the carrier of F -valued Function-like V23( NAT ) V27( NAT , bool the carrier of F) subsequence of G

(F,H) is closed Element of bool the carrier of F

F is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

i is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

H is non empty Relation-like NAT -defined NAT -valued Function-like V23( NAT ) V27( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

F * H is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of F

G * H is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of G

P is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

P is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of G

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . P is Element of bool the carrier of (TOP-REAL 2)

P . P is Element of bool the carrier of (TOP-REAL 2)

dom H is non empty Element of bool NAT

i is set

H . P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

F . (H . P) is Element of bool the carrier of (TOP-REAL 2)

G . (H . P) is Element of bool the carrier of (TOP-REAL 2)

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

i . P is Element of bool the carrier of (TOP-REAL 2)

P . P is Element of bool the carrier of (TOP-REAL 2)

F is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

G is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

i is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

H is non empty Relation-like NAT -defined NAT -valued Function-like V23( NAT ) V27( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

G * H is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of G

F * H is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of F

P is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) Element of bool [:NAT,(bool the carrier of (TOP-REAL 2)):]

P is non empty Relation-like NAT -defined bool the carrier of (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of F

P is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT

P . P is Element of bool the carrier of (TOP-REAL 2)

i . P is Element of bool the carrier of (TOP-REAL 2)

dom H is non empty Element of bool NAT

i is