:: 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₁₁ is set
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₁₁ is open Element of bool the carrier of (TOP-REAL F)
i /\ c₁₁ is Element of bool the carrier of (TOP-REAL F)
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₁₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
c₁₁ + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT
1 / (c₁₁ + 1) is V11() real ext-real non negative Element of REAL
(c₁₁ + 1) " is non empty V11() real ext-real positive non negative set
1 * ((c₁₁ + 1) ") is V11() real ext-real non negative set
Ball (H,(1 / (c₁₁ + 1))) is Element of bool the carrier of (Euclid F)
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₁₁ is Relation-like Function-like V37(F) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL F)
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₁₁) - 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)
K389((P . c₁₁),G) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.((P . c₁₁) - G).| is V11() real ext-real non negative Element of REAL
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₁₁ 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 . c₁₁ 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 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₁₁ is Element of the carrier of F
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₁₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
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₁₁,m) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
(max (c₁₁,m)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative Element of NAT
G . ((max (c₁₁,m)) + 1) is Element of bool the carrier of (TOP-REAL F)
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₁₁ is a_neighborhood of P
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₁₁ 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
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<sub>11</sub> 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
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 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
P . P is Element of bool the carrier of (TOP-REAL 2)
i . 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)):]
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
i is set
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
((TOP-REAL 2),H) is closed Element of bool the carrier of (TOP-REAL 2)
NS 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
((TOP-REAL 2),NS) is closed Element of 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)):]
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)):]
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),F) \/ ((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),i) is Element of bool the carrier of (TOP-REAL 2)
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 (TOP-REAL 2)
i . H is Element of bool the carrier of (TOP-REAL 2)
F . H is Element of bool the carrier of (TOP-REAL 2)
(F . H) \/ (G . H) is Element of bool the carrier of (TOP-REAL 2)
H is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
F . H is Element of bool the carrier of (TOP-REAL 2)
i . H is Element of bool the carrier of (TOP-REAL 2)
G . H is Element of bool the carrier of (TOP-REAL 2)
(F . H) \/ (G . H) is Element of bool the carrier of (TOP-REAL 2)
H is set
NS 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
((TOP-REAL 2),NS) is closed Element of 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 i
((TOP-REAL 2),P) is closed Element of bool the carrier of (TOP-REAL 2)
NS 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
((TOP-REAL 2),NS) is closed Element of 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 i
((TOP-REAL 2),P) is closed Element of 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)):]
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)):]
((TOP-REAL 2),i) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),F) /\ ((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
H is set
NS 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 i
((TOP-REAL 2),NS) is closed 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)
G . P is Element of bool the carrier of (TOP-REAL 2)
F . P is Element of bool the carrier of (TOP-REAL 2)
(F . P) /\ (G . P) is Element of 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
((TOP-REAL 2),P) is closed 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)
F . P is Element of bool the carrier of (TOP-REAL 2)
G . P is Element of bool the carrier of (TOP-REAL 2)
(F . P) /\ (G . P) is Element of 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
((TOP-REAL 2),P) is closed Element of bool the carrier of (TOP-REAL 2)
[:(TOP-REAL 2),(TOP-REAL 2):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty set
bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty Element of bool (bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):])
bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty set
bool (bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) is non empty set
[:NAT,(bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]):] is non empty Relation-like set
bool [:NAT,(bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]):] is non empty 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)):]
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),(TOP-REAL 2):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) Element of bool [:NAT,(bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]):]
H is non empty Relation-like NAT -defined bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) Element of bool [:NAT,(bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]):]
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:]
i * NS is non empty Relation-like NAT -defined bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) subsequence of i
G * NS 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 * NS 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)):]
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)):]
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 [:(TOP-REAL 2),(TOP-REAL 2):]
P . i is Element of bool the carrier of (TOP-REAL 2)
i . i is Element of bool the carrier of (TOP-REAL 2)
[:(P . i),(i . i):] is Relation-like Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
dom NS is non empty Element of bool NAT
NS . i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
F . (NS . i) is Element of bool the carrier of (TOP-REAL 2)
G . (NS . i) is Element of bool the carrier of (TOP-REAL 2)
i . (NS . i) is Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
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 [:(TOP-REAL 2),(TOP-REAL 2):]
P . i is Element of bool the carrier of (TOP-REAL 2)
i . i is Element of bool the carrier of (TOP-REAL 2)
[:(P . i),(i . i):] is Relation-like Element of bool the carrier of [:(TOP-REAL 2),(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)):]
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),G) is Element of bool the carrier of (TOP-REAL 2)
[:((TOP-REAL 2),F),((TOP-REAL 2),G):] is Relation-like Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
i is non empty Relation-like NAT -defined bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) Element of bool [:NAT,(bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]):]
([:(TOP-REAL 2),(TOP-REAL 2):],i) is Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
H is set
NS is non empty Relation-like NAT -defined bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] -valued Function-like V23( NAT ) V27( NAT , bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) subsequence of i
([:(TOP-REAL 2),(TOP-REAL 2):],NS) is closed Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty Relation-like 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 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)):]
((TOP-REAL 2),P) is closed Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),i) is closed Element of bool the carrier of (TOP-REAL 2)
[:((TOP-REAL 2),P),((TOP-REAL 2),i):] is Relation-like Element of bool the carrier of [:(TOP-REAL 2),(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):]
(F,G) is closed Element of bool the carrier of F
(F,G) is Element of bool the carrier of F
i is Element of bool the carrier of F
H is set
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
(F,NS) 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)):]
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
G is Element of bool the carrier of (TOP-REAL 2)
Cl G is closed 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 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)):]
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),G) is Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),F) is Element of bool the carrier of (TOP-REAL 2)
i is set
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
((TOP-REAL 2),H) is closed Element of bool the carrier of (TOP-REAL 2)
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 (TOP-REAL 2) -valued Function-like V23( NAT ) V27( NAT , bool the carrier of (TOP-REAL 2)) subsequence of G
F * NS 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
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 (TOP-REAL 2)
P . i is Element of bool the carrier of (TOP-REAL 2)
Cl (P . i) is closed Element of bool the carrier of (TOP-REAL 2)
dom NS is non empty Element of bool NAT
NS . i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
G . (NS . i) is Element of bool the carrier of (TOP-REAL 2)
F . (NS . i) is Element of bool the carrier of (TOP-REAL 2)
Cl (F . (NS . i)) is closed Element of bool the carrier of (TOP-REAL 2)
((TOP-REAL 2),P) is closed Element of bool the carrier of (TOP-REAL 2)
i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of NAT
F . i is Element of bool the carrier of (TOP-REAL 2)
G . i is Element of bool the carrier of (TOP-REAL 2)
Cl (F . i) is closed Element of bool the carrier of (TOP-REAL 2)