REAL is non trivial non finite non countable set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
[:NAT,REAL:] is non trivial Relation-like non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() set
RAT is countable set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real positive non negative Element of NAT
{0,1} is non empty finite V34() set
bool NAT is non empty non trivial non finite set
[:1,1:] is non empty Relation-like finite set
bool [:1,1:] is non empty finite V34() set
[:[:1,1:],1:] is non empty Relation-like finite set
bool [:[:1,1:],1:] is non empty finite V34() set
[:[:1,1:],REAL:] is non trivial Relation-like non finite set
bool [:[:1,1:],REAL:] is non empty non trivial non finite 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 finite cardinal ext-real positive non negative Element of NAT
[:2,2:] is non empty Relation-like finite set
[:[:2,2:],REAL:] is non trivial Relation-like non finite set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
COMPLEX is set
INT is set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL 2) is non empty set
K585() is non empty strict TopSpace-like V316() TopStruct
the carrier of K585() is non empty V263() set
RealSpace is non empty strict Reflexive discerning V210() triangle Discerning V316() MetrStruct
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V27([:REAL,REAL:], REAL ) V251() V252() V253() Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
R^1 is non empty strict TopSpace-like V316() TopStruct
the carrier of R^1 is non empty V263() set
bool the carrier of R^1 is non empty set
card omega is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() Element of NAT
omega *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
{0} is non empty trivial functional finite V34() 1 -element set
meet 0 is set
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of RealSpace is non empty V263() set
Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is non empty set
bool (bool the carrier of RealSpace) is non empty set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct
-infty is non empty non real ext-real non positive negative set
bool 0 is non empty finite V34() set
union 0 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
dom 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() set
rng 0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative with_non-empty_elements countable V251() V252() V253() V254() V255() V256() V257() V258() V261() V262() V263() V264() V266() set
[:R^1,R^1:] is non empty strict TopSpace-like TopStruct
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
TM is empty trivial finite 0 -element TopSpace-like T_0 T_1 T_2 T_1/2 second-countable TopStruct
M is empty trivial finite 0 -element TopSpace-like T_0 T_1 T_2 T_1/2 second-countable TopStruct
the carrier of TM is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() V255() V256() V257() V258() set
the carrier of M is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() V255() V256() V257() V258() set
[: the carrier of TM, the carrier of M:] is Relation-like finite set
bool [: the carrier of TM, the carrier of M:] is non empty finite V34() set
[#] M is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable dense boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of M
bool the carrier of M is non empty finite V34() set
[#] TM is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable dense boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of TM
bool the carrier of TM is non empty finite V34() set
A1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding the carrier of TM -defined the carrier of M -valued Function-like one-to-one constant functional V27( the carrier of TM, the carrier of M) finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() Element of bool [: the carrier of TM, the carrier of M:]
A1 " is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding the carrier of M -defined the carrier of TM -valued Function-like one-to-one constant functional V27( the carrier of M, the carrier of TM) finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() Element of bool [: the carrier of M, the carrier of TM:]
[: the carrier of M, the carrier of TM:] is Relation-like finite set
bool [: the carrier of M, the carrier of TM:] is non empty finite V34() set
A2 is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of TM
(A1 ") " A2 is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of M
A2 is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of M
A1 " A2 is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of TM
TM is TopSpace-like TopStruct
[#] TM is non proper open closed dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
M is TopSpace-like TopStruct
[#] M is non proper open closed dense Element of bool the carrier of M
the carrier of M is set
bool the carrier of M is non empty set
TM | ([#] TM) is strict TopSpace-like SubSpace of TM
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
TopStruct(# the carrier of TM, the topology of TM #) is strict TopSpace-like TopStruct
M | ([#] M) is strict TopSpace-like SubSpace of M
the topology of M is non empty open Element of bool (bool the carrier of M)
bool (bool the carrier of M) is non empty set
TopStruct(# the carrier of M, the topology of M #) is strict TopSpace-like TopStruct
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
[: the carrier of TM, the carrier of M:] is Relation-like set
bool [: the carrier of TM, the carrier of M:] is non empty set
A1 is Element of bool the carrier of TM
TM | A1 is strict TopSpace-like SubSpace of TM
the carrier of (TM | A1) is set
A2 is Relation-like the carrier of TM -defined the carrier of M -valued Function-like V27( the carrier of TM, the carrier of M) Element of bool [: the carrier of TM, the carrier of M:]
A2 .: A1 is Element of bool the carrier of M
bool the carrier of M is non empty set
M | (A2 .: A1) is strict TopSpace-like SubSpace of M
the carrier of (M | (A2 .: A1)) is set
[: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):] is Relation-like set
bool [: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):] is non empty set
A2 | A1 is Relation-like the carrier of TM -defined A1 -defined the carrier of TM -defined the carrier of M -valued Function-like Element of bool [: the carrier of TM, the carrier of M:]
dom A2 is Element of bool the carrier of TM
[#] TM is non proper open closed dense Element of bool the carrier of TM
[#] M is non proper open closed dense Element of bool the carrier of M
rng A2 is Element of bool the carrier of M
V2 is Relation-like the carrier of (TM | A1) -defined the carrier of (M | (A2 .: A1)) -valued Function-like V27( the carrier of (TM | A1), the carrier of (M | (A2 .: A1))) Element of bool [: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):]
rng V2 is Element of bool the carrier of (M | (A2 .: A1))
bool the carrier of (M | (A2 .: A1)) is non empty set
dom V2 is Element of bool the carrier of (TM | A1)
bool the carrier of (TM | A1) is non empty set
(dom A2) /\ A1 is Element of bool the carrier of TM
[#] (TM | A1) is non proper open closed dense Element of bool the carrier of (TM | A1)
[#] (M | (A2 .: A1)) is non proper open closed dense Element of bool the carrier of (M | (A2 .: A1))
mV2 is Element of bool the carrier of (M | (A2 .: A1))
V2 " mV2 is Element of bool the carrier of (TM | A1)
mL is Element of bool the carrier of M
mL /\ (A2 .: A1) is Element of bool the carrier of M
A2 " mL is Element of bool the carrier of TM
(A2 " mL) /\ A1 is Element of bool the carrier of TM
A2 " (A2 .: A1) is Element of bool the carrier of TM
U9 is Element of bool the carrier of (TM | A1)
A1 /\ U9 is Element of bool the carrier of (TM | A1)
A2 " mV2 is Element of bool the carrier of TM
A2 " is Relation-like the carrier of M -defined the carrier of TM -valued Function-like V27( the carrier of M, the carrier of TM) Element of bool [: the carrier of M, the carrier of TM:]
[: the carrier of M, the carrier of TM:] is Relation-like set
bool [: the carrier of M, the carrier of TM:] is non empty set
V2 " is Relation-like the carrier of (M | (A2 .: A1)) -defined the carrier of (TM | A1) -valued Function-like V27( the carrier of (M | (A2 .: A1)), the carrier of (TM | A1)) Element of bool [: the carrier of (M | (A2 .: A1)), the carrier of (TM | A1):]
[: the carrier of (M | (A2 .: A1)), the carrier of (TM | A1):] is Relation-like set
bool [: the carrier of (M | (A2 .: A1)), the carrier of (TM | A1):] is non empty set
mV2 is Element of bool the carrier of (TM | A1)
(V2 ") " mV2 is Element of bool the carrier of (M | (A2 .: A1))
mL is Element of bool the carrier of TM
mL /\ A1 is Element of bool the carrier of TM
(A2 ") " mL is Element of bool the carrier of M
((A2 ") " mL) /\ (A2 .: A1) is Element of bool the carrier of M
(A2 ") " A1 is Element of bool the carrier of M
U9 is Element of bool the carrier of (M | (A2 .: A1))
(A2 ") " (mL /\ A1) is Element of bool the carrier of M
A2 .: mV2 is Element of bool the carrier of M
V2 .: mV2 is Element of bool the carrier of (M | (A2 .: A1))
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
[: the carrier of TM, the carrier of M:] is Relation-like set
bool [: the carrier of TM, the carrier of M:] is non empty set
A1 is Element of bool the carrier of TM
A2 is Relation-like the carrier of TM -defined the carrier of M -valued Function-like V27( the carrier of TM, the carrier of M) Element of bool [: the carrier of TM, the carrier of M:]
A2 .: A1 is Element of bool the carrier of M
bool the carrier of M is non empty set
dom A2 is Element of bool the carrier of TM
[#] TM is non proper open closed dense Element of bool the carrier of TM
A2 | A1 is Relation-like the carrier of TM -defined A1 -defined the carrier of TM -defined the carrier of M -valued Function-like Element of bool [: the carrier of TM, the carrier of M:]
dom (A2 | A1) is Element of bool A1
bool A1 is non empty set
([#] TM) /\ A1 is Element of bool the carrier of TM
TM | A1 is strict TopSpace-like SubSpace of TM
[#] (TM | A1) is non proper open closed dense Element of bool the carrier of (TM | A1)
the carrier of (TM | A1) is set
bool the carrier of (TM | A1) is non empty set
rng (A2 | A1) is Element of bool the carrier of M
M | (A2 .: A1) is strict TopSpace-like SubSpace of M
[#] (M | (A2 .: A1)) is non proper open closed dense Element of bool the carrier of (M | (A2 .: A1))
the carrier of (M | (A2 .: A1)) is set
bool the carrier of (M | (A2 .: A1)) is non empty set
[: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):] is Relation-like set
bool [: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):] is non empty set
V1 is Relation-like the carrier of (TM | A1) -defined the carrier of (M | (A2 .: A1)) -valued Function-like V27( the carrier of (TM | A1), the carrier of (M | (A2 .: A1))) Element of bool [: the carrier of (TM | A1), the carrier of (M | (A2 .: A1)):]
TM is non empty TopSpace-like TopStruct
M is non empty TopSpace-like TopStruct
weight M is epsilon-transitive epsilon-connected ordinal cardinal set
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is non empty set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
A1 is V65(TM) open Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of M is non empty set
[: the carrier of TM, the carrier of M:] is non empty Relation-like set
bool [: the carrier of TM, the carrier of M:] is non empty set
A2 is Relation-like the carrier of TM -defined the carrier of M -valued Function-like V27( the carrier of TM, the carrier of M) Element of bool [: the carrier of TM, the carrier of M:]
bool the carrier of M is non empty set
{ H1(b1) where b1 is Element of bool the carrier of TM : S2[b1] } is set
card { H1(b1) where b1 is Element of bool the carrier of TM : S2[b1] } is epsilon-transitive epsilon-connected ordinal cardinal set
bool (bool the carrier of M) is non empty set
V1 is Element of bool (bool the carrier of M)
V2 is Element of bool the carrier of M
A2 " V2 is Element of bool the carrier of TM
TMM is Element of the carrier of M
rng A2 is Element of bool the carrier of M
[#] M is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of M
dom A2 is Element of bool the carrier of TM
mV1 is set
A2 . mV1 is set
mV2 is Element of the carrier of TM
mL is Element of bool the carrier of TM
A2 .: mL is Element of bool the carrier of M
U9 is Element of bool the carrier of M
A2 .: (A2 " V2) is Element of bool the carrier of M
the topology of TM is non empty open Element of bool (bool the carrier of TM)
the topology of M is non empty open Element of bool (bool the carrier of M)
V2 is set
TMM is Element of bool the carrier of TM
A2 .: TMM is Element of bool the carrier of M
V2 is V65(M) open Element of bool (bool the carrier of M)
card V2 is epsilon-transitive epsilon-connected ordinal cardinal set
TM is empty trivial finite 0 -element TopSpace-like T_0 T_1 T_2 T_1/2 second-countable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() V255() V256() V257() V258() set
bool the carrier of TM is non empty finite V34() set
bool (bool the carrier of TM) is non empty finite V34() set
M is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() open closed Element of bool (bool the carrier of TM)
the topology of TM is non empty finite V34() open Element of bool (bool the carrier of TM)
A1 is empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() V255() V256() V257() V258() Element of bool the carrier of TM
A2 is epsilon-transitive epsilon-connected ordinal natural V11() real Relation-like Function-like finite cardinal ext-real Element of the carrier of TM
A1 is finite V34() V65(TM) open Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of omega
TM is TopSpace-like TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is TopSpace-like TopStruct
weight M is epsilon-transitive epsilon-connected ordinal cardinal set
[#] TM is non proper open closed dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
[#] M is non proper open closed dense Element of bool the carrier of M
the carrier of M is set
bool the carrier of M is non empty set
[#] TM is non proper open closed dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
[#] M is non proper open closed dense Element of bool the carrier of M
the carrier of M is set
bool the carrier of M is non empty set
TM is TopSpace-like TopStruct
the carrier of TM is set
rng 0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative with_non-empty_elements countable V251() V252() V253() V254() V255() V256() V257() V258() V261() V262() V263() V264() V266() Element of bool RAT
bool RAT is non empty set
bool the carrier of TM is non empty Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
A1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,A1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,A1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1)))
the carrier of (SpaceMetr ( the carrier of TM,A1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,A1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1))) is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
V1 is Element of the carrier of TM
V2 is Element of the carrier of TM
A1 . (V1,V2) is V11() real ext-real Element of REAL
[V1,V2] is set
{V1,V2} is non empty finite set
{V1} is non empty trivial finite 1 -element set
{{V1,V2},{V1}} is non empty finite V34() set
A1 . [V1,V2] is V11() real ext-real set
A1 . (V2,V1) is V11() real ext-real Element of REAL
[V2,V1] is set
{V2,V1} is non empty finite set
{V2} is non empty trivial finite 1 -element set
{{V2,V1},{V2}} is non empty finite V34() set
A1 . [V2,V1] is V11() real ext-real set
TMM is Element of the carrier of TM
A1 . (V1,TMM) is V11() real ext-real Element of REAL
[V1,TMM] is set
{V1,TMM} is non empty finite set
{{V1,TMM},{V1}} is non empty finite V34() set
A1 . [V1,TMM] is V11() real ext-real set
A1 . (V2,TMM) is V11() real ext-real Element of REAL
[V2,TMM] is set
{V2,TMM} is non empty finite set
{{V2,TMM},{V2}} is non empty finite V34() set
A1 . [V2,TMM] is V11() real ext-real set
(A1 . (V1,V2)) + (A1 . (V2,TMM)) is V11() real ext-real set
MetrStruct(# the carrier of TM,A1 #) is strict MetrStruct
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
M is non empty TopSpace-like metrizable TopStruct
the carrier of M is non empty set
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
[:NAT,(bool (bool the carrier of M)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of M)):] is non empty non trivial non finite set
A1 is Relation-like NAT -defined bool (bool the carrier of M) -valued Function-like V27( NAT , bool (bool the carrier of M)) Element of bool [:NAT,(bool (bool the carrier of M)):]
TM is Reflexive discerning V210() triangle MetrStruct
TopSpaceMetr TM is strict TopSpace-like TopStruct
the carrier of TM is set
Family_open_set TM is Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
TopStruct(# the carrier of TM,(Family_open_set TM) #) is strict TopStruct
M is non empty Reflexive discerning V210() triangle Discerning MetrStruct
the carrier of M is non empty set
bool the carrier of M is non empty set
[#] TM is non proper Element of bool the carrier of TM
the carrier of (TopSpaceMetr TM) is set
bool the carrier of (TopSpaceMetr TM) is non empty set
[#] (TopSpaceMetr TM) is non proper open closed dense Element of bool the carrier of (TopSpaceMetr TM)
A2 is non empty Element of bool the carrier of M
M | A2 is non empty strict Reflexive discerning V210() triangle Discerning SubSpace of M
TopSpaceMetr (M | A2) is non empty strict TopSpace-like TopStruct
the carrier of (M | A2) is non empty set
Family_open_set (M | A2) is Element of bool (bool the carrier of (M | A2))
bool the carrier of (M | A2) is non empty set
bool (bool the carrier of (M | A2)) is non empty set
TopStruct(# the carrier of (M | A2),(Family_open_set (M | A2)) #) is non empty strict TopStruct
[#] (M | A2) is non empty non proper Element of bool the carrier of (M | A2)
[: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):] is Relation-like set
[:[: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):],REAL:] is Relation-like set
bool [:[: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):],REAL:] is non empty set
the distance of (M | A2) is Relation-like [: the carrier of (M | A2), the carrier of (M | A2):] -defined REAL -valued Function-like V27([: the carrier of (M | A2), the carrier of (M | A2):], REAL ) V251() V252() V253() Element of bool [:[: the carrier of (M | A2), the carrier of (M | A2):],REAL:]
[: the carrier of (M | A2), the carrier of (M | A2):] is non empty Relation-like set
[:[: the carrier of (M | A2), the carrier of (M | A2):],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of (M | A2), the carrier of (M | A2):],REAL:] is non empty non trivial non finite set
TMM is Relation-like [: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):] -defined REAL -valued Function-like V27([: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):], REAL ) V251() V252() V253() Element of bool [:[: the carrier of (TopSpaceMetr TM), the carrier of (TopSpaceMetr TM):],REAL:]
SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM)))
the carrier of (SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM)) is set
bool the carrier of (SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of (TopSpaceMetr TM),TMM))) is non empty set
the topology of (TopSpaceMetr TM) is non empty open Element of bool (bool the carrier of (TopSpaceMetr TM))
bool (bool the carrier of (TopSpaceMetr TM)) is non empty set
V1 is Element of bool the carrier of (TopSpaceMetr TM)
(TopSpaceMetr TM) | V1 is strict TopSpace-like SubSpace of TopSpaceMetr TM
the topology of (TopSpaceMetr (M | A2)) is non empty open Element of bool (bool the carrier of (TopSpaceMetr (M | A2)))
the carrier of (TopSpaceMetr (M | A2)) is non empty set
bool the carrier of (TopSpaceMetr (M | A2)) is non empty set
bool (bool the carrier of (TopSpaceMetr (M | A2))) is non empty set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
A1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,A1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,A1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1)))
the carrier of (SpaceMetr ( the carrier of TM,A1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,A1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1))) is non empty set
A2 is non empty Reflexive discerning V210() triangle Discerning MetrStruct
the carrier of A2 is non empty set
bool the carrier of A2 is non empty set
TopSpaceMetr A2 is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
Family_open_set A2 is Element of bool (bool the carrier of A2)
bool (bool the carrier of A2) is non empty set
TopStruct(# the carrier of A2,(Family_open_set A2) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr A2) is non empty set
bool the carrier of (TopSpaceMetr A2) is non empty set
V1 is non empty Element of bool the carrier of A2
V2 is non empty Element of bool the carrier of (TopSpaceMetr A2)
(TopSpaceMetr A2) | V2 is non empty strict TopSpace-like T_0 T_1 T_2 T_1/2 SubSpace of TopSpaceMetr A2
A2 | V1 is non empty strict Reflexive discerning V210() triangle Discerning SubSpace of A2
TopSpaceMetr (A2 | V1) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (A2 | V1) is non empty set
Family_open_set (A2 | V1) is Element of bool (bool the carrier of (A2 | V1))
bool the carrier of (A2 | V1) is non empty set
bool (bool the carrier of (A2 | V1)) is non empty set
TopStruct(# the carrier of (A2 | V1),(Family_open_set (A2 | V1)) #) is non empty strict TopStruct
[#] ((TopSpaceMetr A2) | V2) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of ((TopSpaceMetr A2) | V2)
the carrier of ((TopSpaceMetr A2) | V2) is non empty set
bool the carrier of ((TopSpaceMetr A2) | V2) is non empty set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
M is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
[:TM,M:] is strict TopSpace-like TopStruct
the carrier of M is set
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like set
bool [:[: the carrier of M, the carrier of M:],REAL:] is non empty set
the topology of M is non empty open Element of bool (bool the carrier of M)
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
A1 is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like V27([: the carrier of M, the carrier of M:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
SpaceMetr ( the carrier of M,A1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of M,A1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of M,A1)))
the carrier of (SpaceMetr ( the carrier of M,A1)) is set
bool the carrier of (SpaceMetr ( the carrier of M,A1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of M,A1))) is non empty set
the carrier of TM is set
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
V1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,V1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,V1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1)))
the carrier of (SpaceMetr ( the carrier of TM,V1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,V1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1))) is non empty set
TopStruct(# the carrier of M, the topology of M #) is strict TopSpace-like TopStruct
mV1 is non empty MetrStruct
TopSpaceMetr mV1 is non empty strict TopSpace-like TopStruct
the carrier of mV1 is non empty set
Family_open_set mV1 is Element of bool (bool the carrier of mV1)
bool the carrier of mV1 is non empty set
bool (bool the carrier of mV1) is non empty set
TopStruct(# the carrier of mV1,(Family_open_set mV1) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr mV1) is non empty set
the topology of (TopSpaceMetr mV1) is non empty open Element of bool (bool the carrier of (TopSpaceMetr mV1))
bool the carrier of (TopSpaceMetr mV1) is non empty set
bool (bool the carrier of (TopSpaceMetr mV1)) is non empty set
TopStruct(# the carrier of (TopSpaceMetr mV1), the topology of (TopSpaceMetr mV1) #) is non empty strict TopSpace-like TopStruct
TopStruct(# the carrier of TM, the topology of TM #) is strict TopSpace-like TopStruct
TMM is non empty MetrStruct
TopSpaceMetr TMM is non empty strict TopSpace-like TopStruct
the carrier of TMM is non empty set
Family_open_set TMM is Element of bool (bool the carrier of TMM)
bool the carrier of TMM is non empty set
bool (bool the carrier of TMM) is non empty set
TopStruct(# the carrier of TMM,(Family_open_set TMM) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr TMM) is non empty set
the topology of (TopSpaceMetr TMM) is non empty open Element of bool (bool the carrier of (TopSpaceMetr TMM))
bool the carrier of (TopSpaceMetr TMM) is non empty set
bool (bool the carrier of (TopSpaceMetr TMM)) is non empty set
TopStruct(# the carrier of (TopSpaceMetr TMM), the topology of (TopSpaceMetr TMM) #) is non empty strict TopSpace-like TopStruct
[:(TopSpaceMetr TMM),(TopSpaceMetr mV1):] is non empty strict TopSpace-like TopStruct
max-Prod2 (TMM,mV1) is non empty strict MetrStruct
TopSpaceMetr (max-Prod2 (TMM,mV1)) is non empty strict TopSpace-like TopStruct
the carrier of (max-Prod2 (TMM,mV1)) is non empty set
Family_open_set (max-Prod2 (TMM,mV1)) is Element of bool (bool the carrier of (max-Prod2 (TMM,mV1)))
bool the carrier of (max-Prod2 (TMM,mV1)) is non empty set
bool (bool the carrier of (max-Prod2 (TMM,mV1))) is non empty set
TopStruct(# the carrier of (max-Prod2 (TMM,mV1)),(Family_open_set (max-Prod2 (TMM,mV1))) #) is non empty strict TopStruct
TM is empty trivial finite 0 -element TopSpace-like T_0 T_1 T_2 normal T_4 T_1/2 second-countable metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is TopSpace-like TopStruct
[:TM,M:] is strict TopSpace-like TopStruct
weight [:TM,M:] is epsilon-transitive epsilon-connected ordinal cardinal set
weight M is epsilon-transitive epsilon-connected ordinal cardinal set
(weight TM) *` (weight M) is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of M is set
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
A1 is V65(M) open Element of bool (bool the carrier of M)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
A2 is V65(TM) open Element of bool (bool the carrier of TM)
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of [:TM,M:] is set
bool the carrier of [:TM,M:] is non empty set
bool (bool the carrier of [:TM,M:]) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of TM, b2 is Element of bool the carrier of M : ( b1 in A2 & b2 in A1 ) } is set
V1 is V65([:TM,M:]) open Element of bool (bool the carrier of [:TM,M:])
V2 is non empty set
TMM is non empty set
[:V2,TMM:] is non empty Relation-like set
mV1 is non empty set
mV2 is Element of [:V2,TMM:]
mV2 `1 is Element of V2
mV2 `2 is Element of TMM
[:(mV2 `1),(mV2 `2):] is Relation-like set
[:[:V2,TMM:],mV1:] is non empty Relation-like set
bool [:[:V2,TMM:],mV1:] is non empty set
mV2 is Relation-like [:V2,TMM:] -defined mV1 -valued Function-like V27([:V2,TMM:],mV1) Element of bool [:[:V2,TMM:],mV1:]
dom mV2 is Relation-like V2 -defined TMM -valued Element of bool [:V2,TMM:]
bool [:V2,TMM:] is non empty set
rng mV2 is Element of bool mV1
bool mV1 is non empty set
mL is set
U9 is Element of bool the carrier of TM
W9 is Element of bool the carrier of M
[:U9,W9:] is Relation-like Element of bool the carrier of [:TM,M:]
[U9,W9] is Element of [:(bool the carrier of TM),(bool the carrier of M):]
[:(bool the carrier of TM),(bool the carrier of M):] is non empty Relation-like set
{U9,W9} is non empty finite set
{U9} is non empty trivial finite 1 -element set
{{U9,W9},{U9}} is non empty finite V34() set
[U9,W9] `1 is Element of bool the carrier of TM
[U9,W9] `2 is Element of bool the carrier of M
u is Element of [:V2,TMM:]
mV2 . u is Element of mV1
card mV1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card [:V2,TMM:] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card V2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card TMM is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[:(card V2),(card TMM):] is non empty Relation-like set
card [:(card V2),(card TMM):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
(card V2) *` (card TMM) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is TopSpace-like TopStruct
[:TM,M:] is strict TopSpace-like TopStruct
weight [:TM,M:] is epsilon-transitive epsilon-connected ordinal cardinal set
weight M is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
the carrier of M is set
pr2 ( the carrier of TM, the carrier of M) is Relation-like [: the carrier of TM, the carrier of M:] -defined the carrier of M -valued Function-like V27([: the carrier of TM, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of TM, the carrier of M:], the carrier of M:]
[: the carrier of TM, the carrier of M:] is Relation-like set
[:[: the carrier of TM, the carrier of M:], the carrier of M:] is Relation-like set
bool [:[: the carrier of TM, the carrier of M:], the carrier of M:] is non empty set
pr1 ( the carrier of TM, the carrier of M) is Relation-like [: the carrier of TM, the carrier of M:] -defined the carrier of TM -valued Function-like V27([: the carrier of TM, the carrier of M:], the carrier of TM) Element of bool [:[: the carrier of TM, the carrier of M:], the carrier of TM:]
[:[: the carrier of TM, the carrier of M:], the carrier of TM:] is Relation-like set
bool [:[: the carrier of TM, the carrier of M:], the carrier of TM:] is non empty set
V1 is non empty TopSpace-like TopStruct
V2 is non empty TopSpace-like TopStruct
[:V1,V2:] is non empty strict TopSpace-like TopStruct
TMM is non empty TopSpace-like TopStruct
the carrier of TMM is non empty set
bool the carrier of TMM is non empty set
bool (bool the carrier of TMM) is non empty set
weight TMM is epsilon-transitive epsilon-connected ordinal cardinal set
mV1 is V65(TMM) open Element of bool (bool the carrier of TMM)
card mV1 is epsilon-transitive epsilon-connected ordinal cardinal set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
{ H1(b1) where b1 is Element of bool the carrier of TMM : S2[b1] } is set
mV2 is Element of bool (bool the carrier of TM)
the topology of TMM is non empty open Element of bool (bool the carrier of TMM)
the topology of TM is non empty open Element of bool (bool the carrier of TM)
mL is set
U9 is Element of bool the carrier of TMM
(pr1 ( the carrier of TM, the carrier of M)) .: U9 is Element of bool the carrier of TM
mL is Element of bool the carrier of TM
[#] M is non proper open closed dense Element of bool the carrier of M
bool the carrier of M is non empty set
[:mL,([#] M):] is Relation-like Element of bool the carrier of [:TM,M:]
the carrier of [:TM,M:] is set
bool the carrier of [:TM,M:] is non empty set
the Element of the carrier of M is Element of the carrier of M
[#] V2 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of V2
the carrier of V2 is non empty set
bool the carrier of V2 is non empty set
W9 is Element of the carrier of TM
[W9, the Element of the carrier of M] is set
{W9, the Element of the carrier of M} is non empty finite set
{W9} is non empty trivial finite 1 -element set
{{W9, the Element of the carrier of M},{W9}} is non empty finite V34() set
u is Element of the carrier of TMM
w is Element of bool the carrier of TMM
[#] V1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of V1
the carrier of V1 is non empty set
bool the carrier of V1 is non empty set
(pr1 ( the carrier of TM, the carrier of M)) . (W9, the Element of the carrier of M) is set
(pr1 ( the carrier of TM, the carrier of M)) . [W9, the Element of the carrier of M] is set
(pr1 ( the carrier of TM, the carrier of M)) .: w is Element of bool the carrier of TM
u1 is open Element of bool the carrier of TM
dom (pr1 ( the carrier of TM, the carrier of M)) is Relation-like the carrier of TM -defined the carrier of M -valued Element of bool [: the carrier of TM, the carrier of M:]
bool [: the carrier of TM, the carrier of M:] is non empty set
[#] TM is non proper open closed dense Element of bool the carrier of TM
[:([#] TM),([#] M):] is Relation-like Element of bool the carrier of [:TM,M:]
[#] TMM is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of TMM
w1 is set
U1 is set
(pr1 ( the carrier of TM, the carrier of M)) . U1 is set
W1 is set
L is set
[W1,L] is set
{W1,L} is non empty finite set
{W1} is non empty trivial finite 1 -element set
{{W1,L},{W1}} is non empty finite V34() set
(pr1 ( the carrier of TM, the carrier of M)) . (W1,L) is set
(pr1 ( the carrier of TM, the carrier of M)) . [W1,L] is set
card { H1(b1) where b1 is Element of bool the carrier of TMM : S2[b1] } is epsilon-transitive epsilon-connected ordinal cardinal set
weight V1 is epsilon-transitive epsilon-connected ordinal cardinal set
mL is V65(TM) open Element of bool (bool the carrier of TM)
card mL is epsilon-transitive epsilon-connected ordinal cardinal set
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
{ H2(b1) where b1 is Element of bool the carrier of TMM : S2[b1] } is set
U9 is Element of bool (bool the carrier of M)
W9 is Element of bool the carrier of M
[#] TM is non proper open closed dense Element of bool the carrier of TM
[:([#] TM),W9:] is Relation-like Element of bool the carrier of [:TM,M:]
the carrier of [:TM,M:] is set
bool the carrier of [:TM,M:] is non empty set
the Element of the carrier of TM is Element of the carrier of TM
[#] V1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of V1
the carrier of V1 is non empty set
bool the carrier of V1 is non empty set
w is Element of the carrier of M
[ the Element of the carrier of TM,w] is set
{ the Element of the carrier of TM,w} is non empty finite set
{ the Element of the carrier of TM} is non empty trivial finite 1 -element set
{{ the Element of the carrier of TM,w},{ the Element of the carrier of TM}} is non empty finite V34() set
u1 is Element of the carrier of TMM
w1 is Element of bool the carrier of TMM
[#] V2 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of V2
the carrier of V2 is non empty set
bool the carrier of V2 is non empty set
(pr2 ( the carrier of TM, the carrier of M)) . ( the Element of the carrier of TM,w) is set
(pr2 ( the carrier of TM, the carrier of M)) . [ the Element of the carrier of TM,w] is set
(pr2 ( the carrier of TM, the carrier of M)) .: w1 is Element of bool the carrier of M
U1 is open Element of bool the carrier of M
dom (pr2 ( the carrier of TM, the carrier of M)) is Relation-like the carrier of TM -defined the carrier of M -valued Element of bool [: the carrier of TM, the carrier of M:]
bool [: the carrier of TM, the carrier of M:] is non empty set
[#] M is non proper open closed dense Element of bool the carrier of M
[:([#] TM),([#] M):] is Relation-like Element of bool the carrier of [:TM,M:]
[#] TMM is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of TMM
W1 is set
L is set
(pr2 ( the carrier of TM, the carrier of M)) . L is set
u is set
x2 is set
[u,x2] is set
{u,x2} is non empty finite set
{u} is non empty trivial finite 1 -element set
{{u,x2},{u}} is non empty finite V34() set
(pr2 ( the carrier of TM, the carrier of M)) . (u,x2) is set
(pr2 ( the carrier of TM, the carrier of M)) . [u,x2] is set
the topology of M is non empty open Element of bool (bool the carrier of M)
W9 is set
u is Element of bool the carrier of TMM
(pr2 ( the carrier of TM, the carrier of M)) .: u is Element of bool the carrier of M
card { H2(b1) where b1 is Element of bool the carrier of TMM : S2[b1] } is epsilon-transitive epsilon-connected ordinal cardinal set
W9 is V65(M) open Element of bool (bool the carrier of M)
card W9 is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like second-countable TopStruct
M is TopSpace-like second-countable TopStruct
[:TM,M:] is strict TopSpace-like TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
weight M is epsilon-transitive epsilon-connected ordinal cardinal set
(weight TM) *` (weight M) is epsilon-transitive epsilon-connected ordinal cardinal set
weight [:TM,M:] is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is Element of bool the carrier of TM
A1 is Element of bool (bool the carrier of TM)
A1 | M is Element of bool (bool the carrier of (TM | M))
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
bool (bool the carrier of (TM | M)) is non empty set
card (A1 | M) is epsilon-transitive epsilon-connected ordinal cardinal set
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
[#] (TM | M) is non proper open closed dense Element of bool the carrier of (TM | M)
V1 is set
V1 /\ M is Element of bool the carrier of TM
[:A1,(A1 | M):] is Relation-like set
bool [:A1,(A1 | M):] is non empty set
V1 is Relation-like A1 -defined A1 | M -valued Function-like V27(A1,A1 | M) Element of bool [:A1,(A1 | M):]
dom V1 is Element of bool A1
bool A1 is non empty set
rng V1 is Element of bool (A1 | M)
bool (A1 | M) is non empty set
V2 is set
TMM is Element of bool the carrier of TM
TMM /\ M is Element of bool the carrier of TM
V1 . TMM is set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
bool (bool the carrier of (TM | M)) is non empty set
A1 is V65(TM) open Element of bool (bool the carrier of TM)
A1 | M is Element of bool (bool the carrier of (TM | M))
V2 is Element of bool the carrier of (TM | M)
TMM is Element of bool the carrier of TM
TMM /\ the carrier of (TM | M) is Element of bool the carrier of TM
mV1 is Element of the carrier of (TM | M)
mV2 is Element of bool the carrier of TM
mV2 /\ M is Element of bool the carrier of TM
[#] (TM | M) is non proper open closed dense Element of bool the carrier of (TM | M)
mL is Element of bool the carrier of (TM | M)
the topology of (TM | M) is non empty open Element of bool (bool the carrier of (TM | M))
V2 is set
TMM is Element of bool the carrier of (TM | M)
TM is TopSpace-like second-countable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
bool (bool the carrier of TM) is non empty set
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is V65(TM) open Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 | M is Element of bool (bool the carrier of (TM | M))
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
bool (bool the carrier of (TM | M)) is non empty set
weight (TM | M) is epsilon-transitive epsilon-connected ordinal cardinal set
card (A1 | M) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is non empty Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr TM is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of TM is non empty set
Family_open_set TM is Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
TopStruct(# the carrier of TM,(Family_open_set TM) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr TM) is non empty set
bool the carrier of (TopSpaceMetr TM) is non empty set
M is non empty Element of bool the carrier of (TopSpaceMetr TM)
dist_min M is Relation-like the carrier of (TopSpaceMetr TM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TM), the carrier of R^1) V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:]
[: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty set
V1 is Element of bool the carrier of R^1
(dist_min M) " V1 is Element of bool the carrier of (TopSpaceMetr TM)
the carrier of (TopSpaceMetr RealSpace) is non empty set
bool the carrier of (TopSpaceMetr RealSpace) is non empty set
TMM is Element of the carrier of TM
(dist_min M) . TMM is V11() real ext-real set
mV1 is Element of the carrier of RealSpace
V2 is open Element of bool the carrier of (TopSpaceMetr RealSpace)
mV2 is V11() real ext-real set
Ball (mV1,mV2) is Element of bool the carrier of RealSpace
Ball (TMM,mV2) is Element of bool the carrier of TM
mL is set
U9 is Element of the carrier of TM
dist (TMM,U9) is V11() real ext-real Element of REAL
the distance of TM is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
[: the carrier of TM, the carrier of TM:] is non empty Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty non trivial non finite set
the distance of TM . (TMM,U9) is V11() real ext-real Element of REAL
[TMM,U9] is set
{TMM,U9} is non empty finite set
{TMM} is non empty trivial finite 1 -element set
{{TMM,U9},{TMM}} is non empty finite V34() set
the distance of TM . [TMM,U9] is V11() real ext-real set
dom (dist_min M) is Element of bool the carrier of (TopSpaceMetr TM)
[#] TM is non empty non proper Element of bool the carrier of TM
(dist_min M) . U9 is V11() real ext-real set
rng (dist_min M) is V261() V262() V263() Element of bool the carrier of R^1
dist (U9,TMM) is V11() real ext-real Element of REAL
the distance of TM . (U9,TMM) is V11() real ext-real Element of REAL
[U9,TMM] is set
{U9,TMM} is non empty finite set
{U9} is non empty trivial finite 1 -element set
{{U9,TMM},{U9}} is non empty finite V34() set
the distance of TM . [U9,TMM] is V11() real ext-real set
(dist (U9,TMM)) + ((dist_min M) . TMM) is V11() real ext-real set
((dist_min M) . U9) - ((dist_min M) . TMM) is V11() real ext-real set
- (dist (TMM,U9)) is V11() real ext-real set
- (((dist_min M) . U9) - ((dist_min M) . TMM)) is V11() real ext-real set
(dist (TMM,U9)) + ((dist_min M) . U9) is V11() real ext-real set
((dist_min M) . TMM) - ((dist_min M) . U9) is V11() real ext-real set
abs (((dist_min M) . TMM) - ((dist_min M) . U9)) is V11() real ext-real Element of REAL
W9 is Element of the carrier of RealSpace
dist (mV1,W9) is V11() real ext-real Element of REAL
the distance of RealSpace is Relation-like [: the carrier of RealSpace, the carrier of RealSpace:] -defined REAL -valued Function-like V27([: the carrier of RealSpace, the carrier of RealSpace:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:]
[: the carrier of RealSpace, the carrier of RealSpace:] is non empty Relation-like V251() V252() V253() set
[:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is non empty non trivial non finite set
the distance of RealSpace . (mV1,W9) is V11() real ext-real Element of REAL
[mV1,W9] is set
{mV1,W9} is non empty finite set
{mV1} is non empty trivial finite 1 -element set
{{mV1,W9},{mV1}} is non empty finite V34() set
the distance of RealSpace . [mV1,W9] is V11() real ext-real set
[#] R^1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of R^1
[#] (TopSpaceMetr TM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TM)
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
A1 is Element of bool the carrier of TM
TM | A1 is strict TopSpace-like SubSpace of TM
A2 is Element of bool the carrier of (TM | M)
(TM | M) | A2 is strict TopSpace-like SubSpace of TM | M
[#] ((TM | M) | A2) is non proper open closed dense Element of bool the carrier of ((TM | M) | A2)
the carrier of ((TM | M) | A2) is set
bool the carrier of ((TM | M) | A2) is non empty set
TM is non empty Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr TM is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of TM is non empty set
Family_open_set TM is Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
TopStruct(# the carrier of TM,(Family_open_set TM) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr TM) is non empty set
bool the carrier of (TopSpaceMetr TM) is non empty set
A1 is non empty Element of bool the carrier of (TopSpaceMetr TM)
dist_min A1 is Relation-like the carrier of (TopSpaceMetr TM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TM), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:]
[: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty set
A2 is V11() real ext-real set
{ b1 where b1 is Element of the carrier of (TopSpaceMetr TM) : not A2 <= (dist_min A1) . b1 } is set
].-infty,A2.[ is Element of bool REAL
V2 is Element of bool the carrier of R^1
(dist_min A1) " V2 is Element of bool the carrier of (TopSpaceMetr TM)
mV1 is set
mV2 is Element of the carrier of (TopSpaceMetr TM)
(dist_min A1) . mV2 is V11() real ext-real Element of the carrier of R^1
dom (dist_min A1) is Element of bool the carrier of (TopSpaceMetr TM)
[#] (TopSpaceMetr TM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TM)
mV1 is set
mV2 is Element of the carrier of (TopSpaceMetr TM)
(dist_min A1) . mV2 is V11() real ext-real Element of the carrier of R^1
[#] R^1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of R^1
[#] (TopSpaceMetr TM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TM)
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
A2 is Element of bool the carrier of TM
V1 is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() open closed Element of bool (bool the carrier of TM)
union V1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of bool the carrier of TM
[#] TM is non proper open closed dense Element of bool the carrier of TM
[#] TM is non proper open closed dense Element of bool the carrier of TM
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
V1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,V1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,V1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1)))
the carrier of (SpaceMetr ( the carrier of TM,V1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,V1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1))) is non empty set
V2 is non empty Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr V2 is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of V2 is non empty set
Family_open_set V2 is Element of bool (bool the carrier of V2)
bool the carrier of V2 is non empty set
bool (bool the carrier of V2) is non empty set
TopStruct(# the carrier of V2,(Family_open_set V2) #) is non empty strict TopStruct
the topology of (TopSpaceMetr V2) is non empty open Element of bool (bool the carrier of (TopSpaceMetr V2))
the carrier of (TopSpaceMetr V2) is non empty set
bool the carrier of (TopSpaceMetr V2) is non empty set
bool (bool the carrier of (TopSpaceMetr V2)) is non empty set
{} (TopSpaceMetr V2) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable F_sigma G_delta Borel boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of (TopSpaceMetr V2)
({} (TopSpaceMetr V2)) ` is open closed dense Element of bool the carrier of (TopSpaceMetr V2)
the carrier of (TopSpaceMetr V2) \ ({} (TopSpaceMetr V2)) is set
[#] (TopSpaceMetr V2) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr V2)
mV1 is open Element of bool the carrier of (TopSpaceMetr V2)
mV1 ` is closed Element of bool the carrier of (TopSpaceMetr V2)
the carrier of (TopSpaceMetr V2) \ mV1 is set
mV2 is non empty closed Element of bool the carrier of (TopSpaceMetr V2)
dist_min mV2 is Relation-like the carrier of (TopSpaceMetr V2) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr V2), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr V2), the carrier of R^1:]
[: the carrier of (TopSpaceMetr V2), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (TopSpaceMetr V2), the carrier of R^1:] is non empty set
mL is set
U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ U9) is V11() real ext-real set
{ b1 where b1 is Element of the carrier of (TopSpaceMetr V2) : not 1 / (2 |^ U9) <= (dist_min mV2) . b1 } is set
W9 is open Element of bool the carrier of (TopSpaceMetr V2)
u is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ u is V11() real ext-real Element of REAL
1 / (2 |^ u) is V11() real ext-real set
{ b1 where b1 is Element of the carrier of (TopSpaceMetr V2) : not 1 / (2 |^ u) <= (dist_min mV2) . b1 } is set
[:NAT, the topology of TM:] is non empty non trivial Relation-like non finite set
bool [:NAT, the topology of TM:] is non empty non trivial non finite set
mL is Relation-like NAT -defined the topology of TM -valued Function-like V27( NAT , the topology of TM) Element of bool [:NAT, the topology of TM:]
rng mL is Element of bool the topology of TM
bool the topology of TM is non empty set
U9 is open Element of bool (bool the carrier of TM)
COMPLEMENT U9 is Element of bool (bool the carrier of TM)
dom mL is Element of bool NAT
union (COMPLEMENT U9) is Element of bool the carrier of TM
u is set
w is set
u1 is Element of bool the carrier of TM
u1 ` is Element of bool the carrier of TM
the carrier of TM \ u1 is set
w1 is set
mL . w1 is set
U1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ U1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
(dist_min mV2) . u is V11() real ext-real set
1 / (2 |^ U1) is V11() real ext-real set
{ b1 where b1 is Element of the carrier of (TopSpaceMetr V2) : not 1 / (2 |^ U1) <= (dist_min mV2) . b1 } is set
u is set
Cl mV2 is closed Element of bool the carrier of (TopSpaceMetr V2)
w is Element of the carrier of (TopSpaceMetr V2)
(dist_min mV2) . w is V11() real ext-real Element of the carrier of R^1
u1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ u1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ u1) is V11() real ext-real set
mL . u1 is Element of the topology of TM
w1 is Element of bool the carrier of TM
{ b1 where b1 is Element of the carrier of (TopSpaceMetr V2) : not 1 / (2 |^ u1) <= (dist_min mV2) . b1 } is set
U1 is Element of the carrier of (TopSpaceMetr V2)
(dist_min mV2) . U1 is V11() real ext-real Element of the carrier of R^1
w1 ` is Element of bool the carrier of TM
the carrier of TM \ w1 is set
(w1 `) ` is Element of bool the carrier of TM
the carrier of TM \ (w1 `) is set
[#] TM is non proper open closed dense Element of bool the carrier of TM
M is Element of bool the carrier of TM
bool (bool the carrier of TM) is non empty set
A1 is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() open closed Element of bool (bool the carrier of TM)
meet A1 is Element of bool the carrier of TM
M ` is Element of bool the carrier of TM
the carrier of TM \ M is set
(M `) ` is Element of bool the carrier of TM
the carrier of TM \ (M `) is set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
A1 is Element of bool the carrier of TM
A1 /\ M is Element of bool the carrier of TM
A2 is Element of bool the carrier of (TM | M)
bool (bool the carrier of TM) is non empty set
V1 is countable closed Element of bool (bool the carrier of TM)
union V1 is Element of bool the carrier of TM
V1 | M is Element of bool (bool the carrier of (TM | M))
bool (bool the carrier of (TM | M)) is non empty set
union (V1 | M) is Element of bool the carrier of (TM | M)
V2 is set
TMM is set
mV1 is Element of bool the carrier of TM
mV1 /\ M is Element of bool the carrier of TM
card (V1 | M) is epsilon-transitive epsilon-connected ordinal cardinal set
card V1 is epsilon-transitive epsilon-connected ordinal cardinal set
(A1 /\ M) /\ M is Element of bool the carrier of TM
M /\ M is Element of bool the carrier of TM
A1 /\ (M /\ M) is Element of bool the carrier of TM
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
A1 is Element of bool the carrier of TM
A1 /\ M is Element of bool the carrier of TM
A2 is Element of bool the carrier of (TM | M)
bool (bool the carrier of TM) is non empty set
V1 is countable open Element of bool (bool the carrier of TM)
meet V1 is Element of bool the carrier of TM
V1 | M is Element of bool (bool the carrier of (TM | M))
bool (bool the carrier of (TM | M)) is non empty set
meet (V1 | M) is Element of bool the carrier of (TM | M)
V2 is set
TMM is set
mV1 is Element of bool the carrier of (TM | M)
mV2 is Element of bool the carrier of TM
mV2 /\ M is Element of bool the carrier of TM
mV2 is set
mV2 /\ M is Element of bool the carrier of TM
mV2 is Element of bool the carrier of TM
mV2 /\ M is Element of bool the carrier of TM
card (V1 | M) is epsilon-transitive epsilon-connected ordinal cardinal set
card V1 is epsilon-transitive epsilon-connected ordinal cardinal set
V2 is set
TMM is set
mV1 is Element of bool the carrier of TM
mV1 /\ M is Element of bool the carrier of TM
TMM is set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
Cl M is closed Element of bool the carrier of TM
TM | (Cl M) is strict TopSpace-like SubSpace of TM
the carrier of (TM | (Cl M)) is set
bool the carrier of (TM | (Cl M)) is non empty set
[#] (TM | (Cl M)) is non proper open closed dense Element of bool the carrier of (TM | (Cl M))
A2 is non empty TopSpace-like TopStruct
the carrier of A2 is non empty set
bool the carrier of A2 is non empty set
bool (bool the carrier of A2) is non empty set
{ H1(b1) where b1 is Element of the carrier of A2 : S1[b1] } is set
V1 is Element of bool (bool the carrier of A2)
V2 is Element of bool the carrier of A2
TMM is Element of the carrier of A2
{TMM} is non empty trivial finite 1 -element Element of bool the carrier of A2
mV1 is Element of the carrier of TM
{mV1} is non empty trivial finite 1 -element set
mV2 is Element of bool the carrier of TM
M /\ mV2 is Element of bool the carrier of TM
mL is Element of bool the carrier of TM
Cl mL is closed Element of bool the carrier of TM
mV2 /\ (Cl M) is Element of bool the carrier of TM
union V1 is Element of bool the carrier of A2
V2 is set
TMM is set
mV1 is Element of the carrier of A2
{mV1} is non empty trivial finite 1 -element Element of bool the carrier of A2
V2 is set
{V2} is non empty trivial finite 1 -element set
TM is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
omega *` TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM *` TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
the topology of M is non empty open Element of bool (bool the carrier of M)
A2 is Element of bool the carrier of M
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
A2 ` is Element of bool the carrier of M
the carrier of M \ A2 is set
{(A2 `)} is non empty trivial finite 1 -element Element of bool (bool the carrier of M)
V1 is set
{V1} is non empty trivial finite 1 -element set
V2 is Element of bool the carrier of M
A2 /\ V2 is Element of bool the carrier of M
A2 /\ V2 is Element of bool the carrier of M
[:A2, the topology of M:] is Relation-like set
bool [:A2, the topology of M:] is non empty set
V1 is Relation-like A2 -defined the topology of M -valued Function-like V27(A2, the topology of M) Element of bool [:A2, the topology of M:]
rng V1 is Element of bool the topology of M
bool the topology of M is non empty set
V2 is open Element of bool (bool the carrier of M)
TMM is open Element of bool (bool the carrier of M)
V2 \/ TMM is Element of bool (bool the carrier of M)
[#] M is non proper open closed dense Element of bool the carrier of M
mV1 is open Element of bool (bool the carrier of M)
union mV1 is Element of bool the carrier of M
mV2 is set
dom V1 is Element of bool A2
bool A2 is non empty set
V1 . mV2 is set
{mV2} is non empty trivial finite 1 -element set
A2 /\ (V1 . mV2) is Element of bool the carrier of M
mV2 is Element of bool (bool the carrier of M)
card mV2 is epsilon-transitive epsilon-connected ordinal cardinal set
mV2 \ TMM is Element of bool (bool the carrier of M)
mL is set
mL /\ A2 is Element of bool the carrier of M
dom V1 is Element of bool A2
bool A2 is non empty set
U9 is set
V1 . U9 is set
{U9} is non empty trivial finite 1 -element set
[:(mV2 \ TMM),A2:] is Relation-like set
bool [:(mV2 \ TMM),A2:] is non empty set
mL is Relation-like mV2 \ TMM -defined A2 -valued Function-like V27(mV2 \ TMM,A2) Element of bool [:(mV2 \ TMM),A2:]
dom mL is Element of bool (mV2 \ TMM)
bool (mV2 \ TMM) is non empty set
rng mL is Element of bool A2
bool A2 is non empty set
U9 is set
W9 is Element of bool the carrier of M
mL . W9 is set
{(mL . W9)} is non empty trivial finite 1 -element set
W9 /\ A2 is Element of bool the carrier of M
A2 /\ W9 is Element of bool the carrier of M
card (mV2 \ TMM) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of M is set
bool the carrier of M is non empty set
A1 is Element of bool the carrier of M
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
Cl A1 is closed G_delta Element of bool the carrier of M
A2 is non empty TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of A2 is non empty set
bool the carrier of A2 is non empty set
V1 is non empty closed G_delta Borel Element of bool the carrier of A2
A2 | V1 is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable SubSpace of A2
the carrier of (A2 | V1) is non empty set
bool the carrier of (A2 | V1) is non empty set
bool (bool the carrier of (A2 | V1)) is non empty set
TMM is open F_sigma Borel Element of bool the carrier of (A2 | V1)
mV1 is countable closed Element of bool (bool the carrier of (A2 | V1))
union mV1 is Element of bool the carrier of (A2 | V1)
[:NAT,mV1:] is Relation-like set
bool [:NAT,mV1:] is non empty set
mV2 is Relation-like NAT -defined mV1 -valued Function-like V27( NAT ,mV1) Element of bool [:NAT,mV1:]
rng mV2 is Element of bool mV1
bool mV1 is non empty set
dom mV2 is Element of bool NAT
mL is set
mV2 . mL is set
card (mV2 . mL) is epsilon-transitive epsilon-connected ordinal cardinal set
[#] (A2 | V1) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (A2 | V1)
U9 is Element of bool the carrier of (A2 | V1)
W9 is Element of bool the carrier of M
card (dom mV2) is epsilon-transitive epsilon-connected ordinal cardinal set
Union mV2 is set
rng mV2 is set
union (rng mV2) is set
card (Union mV2) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
bool (bool the carrier of M) is non empty set
A1 is Element of bool (bool the carrier of M)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
[#] M is non proper open closed dense Element of bool the carrier of M
A2 is set
the Element of A2 is Element of A2
[:A1,([#] M):] is Relation-like set
bool [:A1,([#] M):] is non empty set
A2 is Relation-like A1 -defined [#] M -valued Function-like V27(A1, [#] M) Element of bool [:A1,([#] M):]
rng A2 is Element of bool ([#] M)
bool ([#] M) is non empty set
V2 is set
dom A2 is Element of bool A1
bool A1 is non empty set
V1 is Element of bool the carrier of M
V2 is Element of the carrier of M
{V2} is non empty trivial finite 1 -element set
TMM is set
A2 . TMM is set
mV1 is Element of bool the carrier of M
V1 /\ mV1 is Element of bool the carrier of M
mV2 is set
mL is set
A2 . mL is set
the Element of mL is Element of mL
the Element of mV1 is Element of mV1
card V1 is epsilon-transitive epsilon-connected ordinal cardinal set
V2 is set
TMM is set
A2 . V2 is set
A2 . TMM is set
the Element of TMM is Element of TMM
the Element of V2 is Element of V2
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
[#] TM is non proper open closed dense Element of bool the carrier of TM
card ([#] TM) is epsilon-transitive epsilon-connected ordinal cardinal set
M is Element of bool (bool the carrier of TM)
card M is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is set
union M is Element of bool the carrier of TM
A2 is set
[:([#] TM),M:] is Relation-like set
bool [:([#] TM),M:] is non empty set
A1 is Relation-like [#] TM -defined M -valued Function-like V27( [#] TM,M) Element of bool [:([#] TM),M:]
rng A1 is Element of bool M
bool M is non empty set
A2 is Element of bool (bool the carrier of TM)
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
dom A1 is Element of bool ([#] TM)
bool ([#] TM) is non empty set
union A2 is Element of bool the carrier of TM
V1 is set
A1 . V1 is set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
A1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,A1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,A1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1)))
the carrier of (SpaceMetr ( the carrier of TM,A1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,A1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,A1))) is non empty set
A2 is non empty Reflexive discerning V210() triangle Discerning MetrStruct
the carrier of A2 is non empty set
bool the carrier of TM is non empty Element of bool (bool the carrier of TM)
V1 is set
V2 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ V2 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ V2) is V11() real ext-real set
bool the carrier of A2 is non empty set
TMM is V11() real ext-real Element of REAL
mV1 is Element of bool the carrier of A2
TMM / 2 is V11() real ext-real set
{ (Ball (b1,(TMM / 2))) where b1 is Element of the carrier of A2 : b1 in mV1 } is set
mL is set
U9 is Element of the carrier of A2
Ball (U9,(TMM / 2)) is Element of bool the carrier of A2
mL is open Element of bool (bool the carrier of TM)
U9 is set
W9 is Element of the carrier of A2
Ball (W9,(TMM / 2)) is Element of bool the carrier of A2
u is Element of the carrier of A2
Ball (u,(TMM / 2)) is Element of bool the carrier of A2
dist (W9,W9) is V11() real ext-real Element of REAL
the distance of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined REAL -valued Function-like V27([: the carrier of A2, the carrier of A2:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of A2, the carrier of A2:],REAL:]
[: the carrier of A2, the carrier of A2:] is non empty Relation-like set
[:[: the carrier of A2, the carrier of A2:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of A2, the carrier of A2:],REAL:] is non empty non trivial non finite set
the distance of A2 . (W9,W9) is V11() real ext-real Element of REAL
[W9,W9] is set
{W9,W9} is non empty finite set
{W9} is non empty trivial finite 1 -element set
{{W9,W9},{W9}} is non empty finite V34() set
the distance of A2 . [W9,W9] is V11() real ext-real set
dist (u,W9) is V11() real ext-real Element of REAL
the distance of A2 . (u,W9) is V11() real ext-real Element of REAL
[u,W9] is set
{u,W9} is non empty finite set
{u} is non empty trivial finite 1 -element set
{{u,W9},{u}} is non empty finite V34() set
the distance of A2 . [u,W9] is V11() real ext-real set
[:mL,mV1:] is Relation-like set
bool [:mL,mV1:] is non empty set
U9 is Relation-like mL -defined mV1 -valued Function-like V27(mL,mV1) Element of bool [:mL,mV1:]
rng U9 is Element of bool mV1
bool mV1 is non empty set
the Element of the carrier of A2 is Element of the carrier of A2
dom U9 is Element of bool mL
bool mL is non empty set
u is Element of the carrier of A2
Ball (u,TMM) is Element of bool the carrier of A2
W9 is Element of bool the carrier of TM
card W9 is epsilon-transitive epsilon-connected ordinal cardinal set
card mL is epsilon-transitive epsilon-connected ordinal cardinal set
u is Element of bool the carrier of TM
w is Element of bool the carrier of TM
u1 is Element of the carrier of A2
Ball (u1,(TMM / 2)) is Element of bool the carrier of A2
w1 is Element of the carrier of A2
Ball (w1,(TMM / 2)) is Element of bool the carrier of A2
U1 is set
W1 is Element of the carrier of A2
dist (w1,W1) is V11() real ext-real Element of REAL
the distance of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined REAL -valued Function-like V27([: the carrier of A2, the carrier of A2:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of A2, the carrier of A2:],REAL:]
[: the carrier of A2, the carrier of A2:] is non empty Relation-like set
[:[: the carrier of A2, the carrier of A2:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of A2, the carrier of A2:],REAL:] is non empty non trivial non finite set
the distance of A2 . (w1,W1) is V11() real ext-real Element of REAL
[w1,W1] is set
{w1,W1} is non empty finite set
{w1} is non empty trivial finite 1 -element set
{{w1,W1},{w1}} is non empty finite V34() set
the distance of A2 . [w1,W1] is V11() real ext-real set
dist (u1,W1) is V11() real ext-real Element of REAL
the distance of A2 . (u1,W1) is V11() real ext-real Element of REAL
[u1,W1] is set
{u1,W1} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,W1},{u1}} is non empty finite V34() set
the distance of A2 . [u1,W1] is V11() real ext-real set
dist (w1,u1) is V11() real ext-real Element of REAL
the distance of A2 . (w1,u1) is V11() real ext-real Element of REAL
[w1,u1] is set
{w1,u1} is non empty finite set
{{w1,u1},{w1}} is non empty finite V34() set
the distance of A2 . [w1,u1] is V11() real ext-real set
dist (W1,u1) is V11() real ext-real Element of REAL
the distance of A2 . (W1,u1) is V11() real ext-real Element of REAL
[W1,u1] is set
{W1,u1} is non empty finite set
{W1} is non empty trivial finite 1 -element set
{{W1,u1},{W1}} is non empty finite V34() set
the distance of A2 . [W1,u1] is V11() real ext-real set
(dist (w1,W1)) + (dist (W1,u1)) is V11() real ext-real set
(TMM / 2) + (TMM / 2) is V11() real ext-real set
u is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ u is V11() real ext-real Element of REAL
1 / (2 |^ u) is V11() real ext-real set
w is Element of the carrier of A2
u1 is Element of the carrier of A2
Ball (u1,TMM) is Element of bool the carrier of A2
w1 is Element of the carrier of A2
Ball (w1,(TMM / 2)) is Element of bool the carrier of A2
U9 . (Ball (w1,(TMM / 2))) is set
dist (w,w1) is V11() real ext-real Element of REAL
the distance of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined REAL -valued Function-like V27([: the carrier of A2, the carrier of A2:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of A2, the carrier of A2:],REAL:]
[: the carrier of A2, the carrier of A2:] is non empty Relation-like set
[:[: the carrier of A2, the carrier of A2:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of A2, the carrier of A2:],REAL:] is non empty non trivial non finite set
the distance of A2 . (w,w1) is V11() real ext-real Element of REAL
[w,w1] is set
{w,w1} is non empty finite set
{w} is non empty trivial finite 1 -element set
{{w,w1},{w}} is non empty finite V34() set
the distance of A2 . [w,w1] is V11() real ext-real set
w is Element of the carrier of A2
Ball (w,(TMM / 2)) is Element of bool the carrier of A2
dist (w,w) is V11() real ext-real Element of REAL
the distance of A2 . (w,w) is V11() real ext-real Element of REAL
[w,w] is set
{w,w} is non empty finite set
{w} is non empty trivial finite 1 -element set
{{w,w},{w}} is non empty finite V34() set
the distance of A2 . [w,w] is V11() real ext-real set
[:NAT,(bool the carrier of TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of TM):] is non empty non trivial non finite set
V1 is Relation-like NAT -defined bool the carrier of TM -valued Function-like V27( NAT , bool the carrier of TM) Element of bool [:NAT,(bool the carrier of TM):]
Union V1 is Element of bool the carrier of TM
rng V1 is set
union (rng V1) is set
V2 is Element of bool the carrier of TM
TMM is Element of bool the carrier of TM
bool the carrier of A2 is non empty set
mV2 is set
mV1 is Element of bool the carrier of A2
Family_open_set A2 is Element of bool (bool the carrier of A2)
bool (bool the carrier of A2) is non empty set
mL is Element of the carrier of A2
U9 is V11() real ext-real Element of REAL
Ball (mL,U9) is Element of bool the carrier of A2
W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ W9) is V11() real ext-real set
V1 . W9 is Element of bool the carrier of TM
u is Element of bool the carrier of TM
card u is epsilon-transitive epsilon-connected ordinal cardinal set
w is Element of the carrier of A2
dist (mL,w) is V11() real ext-real Element of REAL
the distance of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined REAL -valued Function-like V27([: the carrier of A2, the carrier of A2:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of A2, the carrier of A2:],REAL:]
[: the carrier of A2, the carrier of A2:] is non empty Relation-like set
[:[: the carrier of A2, the carrier of A2:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of A2, the carrier of A2:],REAL:] is non empty non trivial non finite set
the distance of A2 . (mL,w) is V11() real ext-real Element of REAL
[mL,w] is set
{mL,w} is non empty finite set
{mL} is non empty trivial finite 1 -element set
{{mL,w},{mL}} is non empty finite V34() set
the distance of A2 . [mL,w] is V11() real ext-real set
card V2 is epsilon-transitive epsilon-connected ordinal cardinal set
dom V1 is Element of bool NAT
TMM is set
V1 . TMM is set
card (V1 . TMM) is epsilon-transitive epsilon-connected ordinal cardinal set
mV1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
V1 . mV1 is Element of bool the carrier of TM
2 |^ mV1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ mV1) is V11() real ext-real set
mV2 is Element of bool the carrier of TM
card mV2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (dom V1) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` M is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is Element of bool the carrier of TM
card M is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card M) is epsilon-transitive epsilon-connected ordinal cardinal set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
V1 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,V1) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,V1)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1)))
the carrier of (SpaceMetr ( the carrier of TM,V1)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,V1)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,V1))) is non empty set
V2 is non empty Reflexive discerning V210() triangle Discerning MetrStruct
the carrier of V2 is non empty set
bool the topology of TM is non empty Element of bool (bool the topology of TM)
bool the topology of TM is non empty set
bool (bool the topology of TM) is non empty set
TMM is set
mV1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ mV1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ mV1) is V11() real ext-real set
bool the carrier of V2 is non empty set
{ H1(b1) where b1 is Element of the carrier of V2 : S3[b1] } is set
{ H1(b1) where b1 is Element of the carrier of V2 : S4[b1] } is set
card { H1(b1) where b1 is Element of the carrier of V2 : S3[b1] } is epsilon-transitive epsilon-connected ordinal cardinal set
U9 is set
W9 is Element of the carrier of V2
Ball (W9,(1 / (2 |^ mV1))) is Element of bool the carrier of V2
U9 is Element of the carrier of V2
W9 is Element of the carrier of V2
card { H1(b1) where b1 is Element of the carrier of V2 : S4[b1] } is epsilon-transitive epsilon-connected ordinal cardinal set
U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ U9 is V11() real ext-real Element of REAL
1 / (2 |^ U9) is V11() real ext-real set
{ (Ball (b1,(1 / (2 |^ U9)))) where b1 is Element of the carrier of V2 : b1 in M } is set
[:NAT,(bool the topology of TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the topology of TM):] is non empty non trivial non finite set
TMM is Relation-like NAT -defined bool the topology of TM -valued Function-like V27( NAT , bool the topology of TM) Element of bool [:NAT,(bool the topology of TM):]
Union TMM is Element of bool the topology of TM
rng TMM is set
union (rng TMM) is set
mV1 is Element of bool (bool the carrier of TM)
mV2 is Element of bool the carrier of TM
mL is Element of the carrier of TM
U9 is Element of the carrier of V2
W9 is V11() real ext-real Element of REAL
Ball (U9,W9) is Element of bool the carrier of V2
bool the carrier of V2 is non empty set
W9 / 2 is V11() real ext-real set
u is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ u is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ u) is V11() real ext-real set
Ball (U9,(1 / (2 |^ u))) is Element of bool the carrier of V2
dist (U9,U9) is V11() real ext-real Element of REAL
the distance of V2 is Relation-like [: the carrier of V2, the carrier of V2:] -defined REAL -valued Function-like V27([: the carrier of V2, the carrier of V2:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of V2, the carrier of V2:],REAL:]
[: the carrier of V2, the carrier of V2:] is non empty Relation-like set
[:[: the carrier of V2, the carrier of V2:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of V2, the carrier of V2:],REAL:] is non empty non trivial non finite set
the distance of V2 . (U9,U9) is V11() real ext-real Element of REAL
[U9,U9] is set
{U9,U9} is non empty finite set
{U9} is non empty trivial finite 1 -element set
{{U9,U9},{U9}} is non empty finite V34() set
the distance of V2 . [U9,U9] is V11() real ext-real set
w is Element of bool the carrier of TM
u1 is set
w1 is Element of the carrier of V2
Ball (w1,(1 / (2 |^ u))) is Element of bool the carrier of V2
U1 is Element of bool the carrier of TM
TMM . u is Element of bool the topology of TM
{ (Ball (b1,(1 / (2 |^ u)))) where b1 is Element of the carrier of V2 : b1 in M } is set
dist (U9,w1) is V11() real ext-real Element of REAL
the distance of V2 . (U9,w1) is V11() real ext-real Element of REAL
[U9,w1] is set
{U9,w1} is non empty finite set
{{U9,w1},{U9}} is non empty finite V34() set
the distance of V2 . [U9,w1] is V11() real ext-real set
W1 is set
L is Element of the carrier of V2
dist (w1,L) is V11() real ext-real Element of REAL
the distance of V2 . (w1,L) is V11() real ext-real Element of REAL
[w1,L] is set
{w1,L} is non empty finite set
{w1} is non empty trivial finite 1 -element set
{{w1,L},{w1}} is non empty finite V34() set
the distance of V2 . [w1,L] is V11() real ext-real set
dist (U9,L) is V11() real ext-real Element of REAL
the distance of V2 . (U9,L) is V11() real ext-real Element of REAL
[U9,L] is set
{U9,L} is non empty finite set
{{U9,L},{U9}} is non empty finite V34() set
the distance of V2 . [U9,L] is V11() real ext-real set
(dist (U9,w1)) + (dist (w1,L)) is V11() real ext-real set
(W9 / 2) + (W9 / 2) is V11() real ext-real set
card mV1 is epsilon-transitive epsilon-connected ordinal cardinal set
dom TMM is Element of bool NAT
card (dom TMM) is epsilon-transitive epsilon-connected ordinal cardinal set
mV2 is set
TMM . mV2 is set
card (TMM . mV2) is epsilon-transitive epsilon-connected ordinal cardinal set
card (Union TMM) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card A1) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` M is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
A1 is Element of bool (bool the carrier of TM)
A2 is Element of bool (bool the carrier of TM)
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
V1 is Element of bool (bool the carrier of TM)
union V1 is Element of bool the carrier of TM
card V1 is epsilon-transitive epsilon-connected ordinal cardinal set
union A1 is Element of bool the carrier of TM
A2 is open Element of bool (bool the carrier of TM)
union A2 is Element of bool the carrier of TM
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
V1 is Element of bool (bool the carrier of TM)
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
V2 is Element of bool (bool the carrier of TM)
card V2 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
bool (bool the carrier of TM) is non empty set
A1 is Element of bool (bool the carrier of TM)
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
bool (bool the carrier of TM) is non empty set
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
the carrier of TM is set
bool the carrier of TM is non empty set
A1 is Element of bool the carrier of TM
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
bool (bool the carrier of TM) is non empty set
A2 is Element of bool (bool the carrier of TM)
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card A1) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` M is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
A1 is V65(TM) open Element of bool (bool the carrier of TM)
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is V65(TM) open Element of bool (bool the carrier of TM)
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
V2 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,V2) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,V2)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,V2)))
the carrier of (SpaceMetr ( the carrier of TM,V2)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,V2)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,V2))) is non empty set
TMM is non empty Reflexive discerning V210() triangle Discerning MetrStruct
the carrier of TMM is non empty set
mV1 is set
mV2 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ mV2 is V11() real ext-real Element of REAL
1 / (2 |^ mV2) is V11() real ext-real set
{ b1 where b1 is Element of bool the carrier of TM : ( b1 in A1 & ex b2 being Element of the carrier of TMM st b1 c= Ball (b2,(1 / (2 |^ mV2))) ) } is set
U9 is set
W9 is Element of bool the carrier of TM
u is Element of the carrier of TMM
Ball (u,(1 / (2 |^ mV2))) is Element of bool the carrier of TMM
bool the carrier of TMM is non empty set
U9 is Element of bool (bool the carrier of TM)
W9 is open Element of bool (bool the carrier of TM)
union W9 is Element of bool the carrier of TM
u is set
u1 is Element of the carrier of TMM
dist (u1,u1) is V11() real ext-real Element of REAL
the distance of TMM is Relation-like [: the carrier of TMM, the carrier of TMM:] -defined REAL -valued Function-like V27([: the carrier of TMM, the carrier of TMM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TMM, the carrier of TMM:],REAL:]
[: the carrier of TMM, the carrier of TMM:] is non empty Relation-like set
[:[: the carrier of TMM, the carrier of TMM:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of TMM, the carrier of TMM:],REAL:] is non empty non trivial non finite set
the distance of TMM . (u1,u1) is V11() real ext-real Element of REAL
[u1,u1] is set
{u1,u1} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,u1},{u1}} is non empty finite V34() set
the distance of TMM . [u1,u1] is V11() real ext-real set
Ball (u1,(1 / (2 |^ mV2))) is Element of bool the carrier of TMM
bool the carrier of TMM is non empty set
w1 is Element of bool the carrier of TM
Family_open_set TMM is Element of bool (bool the carrier of TMM)
bool (bool the carrier of TMM) is non empty set
w is Element of the carrier of TM
U1 is Element of bool the carrier of TM
u is Element of bool (bool the carrier of TM)
card u is epsilon-transitive epsilon-connected ordinal cardinal set
w is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ w is V11() real ext-real Element of REAL
1 / (2 |^ w) is V11() real ext-real set
{ b1 where b1 is Element of bool the carrier of TM : ( b1 in A1 & ex b2 being Element of the carrier of TMM st b1 c= Ball (b2,(1 / (2 |^ w))) ) } is set
mV1 is Relation-like Function-like set
dom mV1 is set
rng mV1 is set
union (rng mV1) is set
mV2 is set
mL is set
U9 is set
mV1 . U9 is set
W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
2 |^ W9 is V11() real ext-real Element of REAL
1 / (2 |^ W9) is V11() real ext-real set
{ b1 where b1 is Element of bool the carrier of TM : ( b1 in A1 & ex b2 being Element of the carrier of TMM st b1 c= Ball (b2,(1 / (2 |^ W9))) ) } is set
mV1 . W9 is set
u is open Element of bool (bool the carrier of TM)
card u is epsilon-transitive epsilon-connected ordinal cardinal set
u is Element of bool the carrier of TM
w is Element of the carrier of TMM
Ball (w,(1 / (2 |^ W9))) is Element of bool the carrier of TMM
bool the carrier of TMM is non empty set
mV2 is Element of bool (bool the carrier of TM)
mL is Element of bool the carrier of TM
Family_open_set TMM is Element of bool (bool the carrier of TMM)
bool the carrier of TMM is non empty set
bool (bool the carrier of TMM) is non empty set
U9 is Element of the carrier of TM
W9 is Element of the carrier of TMM
u is V11() real ext-real Element of REAL
Ball (W9,u) is Element of bool the carrier of TMM
u / 2 is V11() real ext-real set
w is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ w is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ w) is V11() real ext-real set
{ b1 where b1 is Element of bool the carrier of TM : ( b1 in A1 & ex b2 being Element of the carrier of TMM st b1 c= Ball (b2,(1 / (2 |^ w))) ) } is set
mV1 . w is set
u1 is open Element of bool (bool the carrier of TM)
card u1 is epsilon-transitive epsilon-connected ordinal cardinal set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
union u1 is Element of bool the carrier of TM
w1 is set
U1 is Element of bool the carrier of TM
W1 is set
L is Element of the carrier of TMM
Ball (L,(1 / (2 |^ w))) is Element of bool the carrier of TMM
L is Element of the carrier of TMM
Ball (L,(1 / (2 |^ w))) is Element of bool the carrier of TMM
u is Element of the carrier of TMM
dist (L,u) is V11() real ext-real Element of REAL
the distance of TMM is Relation-like [: the carrier of TMM, the carrier of TMM:] -defined REAL -valued Function-like V27([: the carrier of TMM, the carrier of TMM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TMM, the carrier of TMM:],REAL:]
[: the carrier of TMM, the carrier of TMM:] is non empty Relation-like set
[:[: the carrier of TMM, the carrier of TMM:],REAL:] is non trivial Relation-like non finite set
bool [:[: the carrier of TMM, the carrier of TMM:],REAL:] is non empty non trivial non finite set
the distance of TMM . (L,u) is V11() real ext-real Element of REAL
[L,u] is set
{L,u} is non empty finite set
{L} is non empty trivial finite 1 -element set
{{L,u},{L}} is non empty finite V34() set
the distance of TMM . [L,u] is V11() real ext-real set
dist (L,W9) is V11() real ext-real Element of REAL
the distance of TMM . (L,W9) is V11() real ext-real Element of REAL
[L,W9] is set
{L,W9} is non empty finite set
{{L,W9},{L}} is non empty finite V34() set
the distance of TMM . [L,W9] is V11() real ext-real set
dist (W9,L) is V11() real ext-real Element of REAL
the distance of TMM . (W9,L) is V11() real ext-real Element of REAL
[W9,L] is set
{W9,L} is non empty finite set
{W9} is non empty trivial finite 1 -element set
{{W9,L},{W9}} is non empty finite V34() set
the distance of TMM . [W9,L] is V11() real ext-real set
dist (W9,u) is V11() real ext-real Element of REAL
the distance of TMM . (W9,u) is V11() real ext-real Element of REAL
[W9,u] is set
{W9,u} is non empty finite set
{{W9,u},{W9}} is non empty finite V34() set
the distance of TMM . [W9,u] is V11() real ext-real set
(dist (W9,L)) + (dist (L,u)) is V11() real ext-real set
(u / 2) + (u / 2) is V11() real ext-real set
mL is V65(TM) open Element of bool (bool the carrier of TM)
card mL is epsilon-transitive epsilon-connected ordinal cardinal set
U9 is set
mV1 . U9 is set
card (mV1 . U9) is epsilon-transitive epsilon-connected ordinal cardinal set
W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
2 |^ W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
1 / (2 |^ W9) is V11() real ext-real set
{ b1 where b1 is Element of bool the carrier of TM : ( b1 in A1 & ex b2 being Element of the carrier of TMM st b1 c= Ball (b2,(1 / (2 |^ W9))) ) } is set
mV1 . W9 is set
u is open Element of bool (bool the carrier of TM)
card u is epsilon-transitive epsilon-connected ordinal cardinal set
Union mV1 is set
card (Union mV1) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` M is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is Element of bool (bool the carrier of TM)
A1 is Element of bool (bool the carrier of TM)
A2 is Element of bool (bool the carrier of TM)
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
M is Element of bool (bool the carrier of TM)
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is V65(TM) open Element of bool (bool the carrier of TM)
A1 is Element of bool (bool the carrier of TM)
A1 is V65(TM) open Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is Element of bool (bool the carrier of TM)
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
M is Element of bool (bool the carrier of TM)
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
weight TM is epsilon-transitive epsilon-connected ordinal cardinal set
density TM is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the non empty finite set is non empty finite set
DiscreteSpace the non empty finite set is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
discrete_dist the non empty finite set is Relation-like [: the non empty finite set , the non empty finite set :] -defined REAL -valued Function-like V27([: the non empty finite set , the non empty finite set :], REAL ) finite V251() V252() V253() Element of bool [:[: the non empty finite set , the non empty finite set :],REAL:]
[: the non empty finite set , the non empty finite set :] is non empty Relation-like finite set
[:[: the non empty finite set , the non empty finite set :],REAL:] is non trivial Relation-like non finite set
bool [:[: the non empty finite set , the non empty finite set :],REAL:] is non empty non trivial non finite set
MetrStruct(# the non empty finite set ,(discrete_dist the non empty finite set ) #) is strict MetrStruct
TopSpaceMetr (DiscreteSpace the non empty finite set ) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (DiscreteSpace the non empty finite set ) is non empty set
Family_open_set (DiscreteSpace the non empty finite set ) is Element of bool (bool the carrier of (DiscreteSpace the non empty finite set ))
bool the carrier of (DiscreteSpace the non empty finite set ) is non empty set
bool (bool the carrier of (DiscreteSpace the non empty finite set )) is non empty set
TopStruct(# the carrier of (DiscreteSpace the non empty finite set ),(Family_open_set (DiscreteSpace the non empty finite set )) #) is non empty strict TopStruct
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
M is Element of bool (bool the carrier of TM)
A1 is set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
the topology of TM is non empty open Element of bool (bool the carrier of TM)
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
bool the carrier of TM is non empty Element of bool (bool the carrier of TM)
[:NAT,(bool the carrier of TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of TM):] is non empty non trivial non finite set
A1 is Element of bool the carrier of TM
A2 is open Element of bool the carrier of TM
V1 is set
A2 ` is closed Element of bool the carrier of TM
the carrier of TM \ A2 is set
(A2 `) ` is open Element of bool the carrier of TM
the carrier of TM \ (A2 `) is set
V2 is Element of the carrier of TM
TMM is Element of bool the carrier of TM
mV1 is Element of bool the carrier of TM
mV1 ` is Element of bool the carrier of TM
the carrier of TM \ mV1 is set
Cl (mV1 `) is closed Element of bool the carrier of TM
Cl TMM is closed Element of bool the carrier of TM
mV2 is Element of the carrier of TM
[:A1, the topology of TM:] is Relation-like set
bool [:A1, the topology of TM:] is non empty set
V1 is Relation-like A1 -defined the topology of TM -valued Function-like V27(A1, the topology of TM) Element of bool [:A1, the topology of TM:]
A1 ` is Element of bool the carrier of TM
the carrier of TM \ A1 is set
{(A1 `)} is non empty trivial finite 1 -element Element of bool (bool the carrier of TM)
rng V1 is Element of bool the topology of TM
bool the topology of TM is non empty set
V2 is open Element of bool (bool the carrier of TM)
TMM is open Element of bool (bool the carrier of TM)
V2 \/ TMM is Element of bool (bool the carrier of TM)
dom V1 is Element of bool A1
bool A1 is non empty set
[#] TM is non proper open closed dense Element of bool the carrier of TM
union (V2 \/ TMM) is Element of bool the carrier of TM
mV2 is set
V1 . mV2 is set
mL is Element of bool the carrier of TM
Cl mL is closed Element of bool the carrier of TM
mV2 is Element of bool (bool the carrier of TM)
union mV2 is Element of bool the carrier of TM
mV2 \ TMM is Element of bool (bool the carrier of TM)
union TMM is Element of bool the carrier of TM
[:NAT,(bool the carrier of TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of TM):] is non empty non trivial non finite set
{} TM is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of TM
NAT --> ({} TM) is Relation-like NAT -defined bool the carrier of TM -valued Function-like V27( NAT , bool the carrier of TM) V251() V252() V253() V254() Element of bool [:NAT,(bool the carrier of TM):]
mL is Relation-like NAT -defined bool the carrier of TM -valued Function-like V27( NAT , bool the carrier of TM) V251() V252() V253() V254() Element of bool [:NAT,(bool the carrier of TM):]
Union mL is Element of bool the carrier of TM
rng mL is V261() V262() V263() V266() set
union (rng mL) is set
rng mL is V261() V262() V263() V266() Element of bool (bool the carrier of TM)
{({} TM)} is non empty trivial functional finite V34() 1 -element Element of bool (bool the carrier of TM)
({} TM) ` is open closed dense Element of bool the carrier of TM
the carrier of TM \ ({} TM) is set
U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
mL . U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of bool the carrier of TM
Cl (mL . U9) is closed Element of bool the carrier of TM
mL . U9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of bool the carrier of TM
Cl (mL . U9) is closed Element of bool the carrier of TM
mV2 \ TMM is Element of bool (bool the carrier of TM)
[:NAT,(mV2 \ TMM):] is Relation-like set
bool [:NAT,(mV2 \ TMM):] is non empty set
mL is Relation-like NAT -defined mV2 \ TMM -valued Function-like V27( NAT ,mV2 \ TMM) Element of bool [:NAT,(mV2 \ TMM):]
rng mL is Element of bool (mV2 \ TMM)
bool (mV2 \ TMM) is non empty set
U9 is Relation-like NAT -defined bool the carrier of TM -valued Function-like V27( NAT , bool the carrier of TM) Element of bool [:NAT,(bool the carrier of TM):]
Union U9 is Element of bool the carrier of TM
rng U9 is set
union (rng U9) is set
W9 is set
u is set
rng U9 is Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
dom U9 is Element of bool NAT
w is set
U9 . w is set
dom U9 is Element of bool NAT
W9 is set
u is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
U9 . u is Element of bool the carrier of TM
w is set
V1 . w is set
u1 is Element of bool the carrier of TM
Cl u1 is closed Element of bool the carrier of TM
W9 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
U9 . W9 is Element of bool the carrier of TM
Cl (U9 . W9) is closed Element of bool the carrier of TM
u is set
V1 . u is set
w is Element of bool the carrier of TM
Cl w is closed Element of bool the carrier of TM
mV2 \ TMM is Element of bool (bool the carrier of TM)
TM is TopSpace-like TopStruct
[#] TM is non proper open closed dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
card ([#] TM) is epsilon-transitive epsilon-connected ordinal cardinal set
bool (bool the carrier of TM) is non empty set
M is Element of bool (bool the carrier of TM)
A1 is Element of bool (bool the carrier of TM)
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
TOP-REAL 1 is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL 1) is non empty set
the topology of (TOP-REAL 1) is non empty open Element of bool (bool the carrier of (TOP-REAL 1))
bool the carrier of (TOP-REAL 1) is non empty set
bool (bool the carrier of (TOP-REAL 1)) is non empty set
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is non empty strict TopSpace-like TopStruct
Euclid 1 is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid 1) is non empty set
Family_open_set (Euclid 1) is Element of bool (bool the carrier of (Euclid 1))
bool the carrier of (Euclid 1) is non empty set
bool (bool the carrier of (Euclid 1)) is non empty set
TopStruct(# the carrier of (Euclid 1),(Family_open_set (Euclid 1)) #) is non empty strict TopStruct
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real positive non negative Element of NAT
TOP-REAL (1 + 1) is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL (1 + 1)) is non empty set
the topology of (TOP-REAL (1 + 1)) is non empty open Element of bool (bool the carrier of (TOP-REAL (1 + 1)))
bool the carrier of (TOP-REAL (1 + 1)) is non empty set
bool (bool the carrier of (TOP-REAL (1 + 1))) is non empty set
TopStruct(# the carrier of (TOP-REAL (1 + 1)), the topology of (TOP-REAL (1 + 1)) #) is non empty strict TopSpace-like TopStruct
Euclid (1 + 1) is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr (Euclid (1 + 1)) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid (1 + 1)) is non empty set
Family_open_set (Euclid (1 + 1)) is Element of bool (bool the carrier of (Euclid (1 + 1)))
bool the carrier of (Euclid (1 + 1)) is non empty set
bool (bool the carrier of (Euclid (1 + 1))) is non empty set
TopStruct(# the carrier of (Euclid (1 + 1)),(Family_open_set (Euclid (1 + 1))) #) is non empty strict TopStruct
[:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] is non empty strict TopSpace-like TopStruct
weight [:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] is epsilon-transitive epsilon-connected ordinal cardinal set
the topology of (TOP-REAL 2) is non empty open Element of bool (bool the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is non empty set
bool (bool the carrier of (TOP-REAL 2)) is non empty set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
weight TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is Element of bool the carrier of R^1
Cl TM is closed Element of bool the carrier of R^1
[#] R^1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of R^1
weight [:R^1,R^1:] is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of [:R^1,R^1:] is non empty set
the topology of [:R^1,R^1:] is non empty open Element of bool (bool the carrier of [:R^1,R^1:])
bool the carrier of [:R^1,R^1:] is non empty set
bool (bool the carrier of [:R^1,R^1:]) is non empty set
TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #) is non empty strict TopSpace-like TopStruct
weight TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #) is epsilon-transitive epsilon-connected ordinal cardinal set
weight TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is epsilon-transitive epsilon-connected ordinal cardinal set
TM is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
TOP-REAL TM is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL TM) is non empty set
the topology of (TOP-REAL TM) is non empty open Element of bool (bool the carrier of (TOP-REAL TM))
bool the carrier of (TOP-REAL TM) is non empty set
bool (bool the carrier of (TOP-REAL TM)) is non empty set
TopStruct(# the carrier of (TOP-REAL TM), the topology of (TOP-REAL TM) #) is non empty strict TopSpace-like TopStruct
M is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real set
TOP-REAL M is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL M) is non empty set
the topology of (TOP-REAL M) is non empty open Element of bool (bool the carrier of (TOP-REAL M))
bool the carrier of (TOP-REAL M) is non empty set
bool (bool the carrier of (TOP-REAL M)) is non empty set
TopStruct(# the carrier of (TOP-REAL M), the topology of (TOP-REAL M) #) is non empty strict TopSpace-like TopStruct
M + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real finite cardinal ext-real Element of NAT
TOP-REAL (M + 1) is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
the carrier of (TOP-REAL (M + 1)) is non empty set
the topology of (TOP-REAL (M + 1)) is non empty open Element of bool (bool the carrier of (TOP-REAL (M + 1)))
bool the carrier of (TOP-REAL (M + 1)) is non empty set
bool (bool the carrier of (TOP-REAL (M + 1))) is non empty set
TopStruct(# the carrier of (TOP-REAL (M + 1)), the topology of (TOP-REAL (M + 1)) #) is non empty strict TopSpace-like TopStruct
Euclid (M + 1) is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr (Euclid (M + 1)) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid (M + 1)) is non empty set
Family_open_set (Euclid (M + 1)) is Element of bool (bool the carrier of (Euclid (M + 1)))
bool the carrier of (Euclid (M + 1)) is non empty set
bool (bool the carrier of (Euclid (M + 1))) is non empty set
TopStruct(# the carrier of (Euclid (M + 1)),(Family_open_set (Euclid (M + 1))) #) is non empty strict TopStruct
[:TopStruct(# the carrier of (TOP-REAL M), the topology of (TOP-REAL M) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] is non empty strict TopSpace-like TopStruct
weight [:TopStruct(# the carrier of (TOP-REAL M), the topology of (TOP-REAL M) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] is epsilon-transitive epsilon-connected ordinal cardinal set
Euclid M is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr (Euclid M) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid M) is non empty set
Family_open_set (Euclid M) is Element of bool (bool the carrier of (Euclid M))
bool the carrier of (Euclid M) is non empty set
bool (bool the carrier of (Euclid M)) is non empty set
TopStruct(# the carrier of (Euclid M),(Family_open_set (Euclid M)) #) is non empty strict TopStruct
Euclid 1 is non empty strict Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid 1) is non empty set
Family_open_set (Euclid 1) is Element of bool (bool the carrier of (Euclid 1))
bool the carrier of (Euclid 1) is non empty set
bool (bool the carrier of (Euclid 1)) is non empty set
TopStruct(# the carrier of (Euclid 1),(Family_open_set (Euclid 1)) #) is non empty strict TopStruct
weight TopStruct(# the carrier of (TOP-REAL (M + 1)), the topology of (TOP-REAL (M + 1)) #) is epsilon-transitive epsilon-connected ordinal cardinal set
TOP-REAL 0 is non empty TopSpace-like V227() V273() V274() V275() V276() V277() V278() V279() V285() L20()
[#] (TOP-REAL 0) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
bool the carrier of (TOP-REAL 0) is non empty set
REAL 0 is non empty FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
<*> REAL is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V251() V252() V253() FinSequence of REAL
{(<*> REAL)} is non empty trivial functional finite 1 -element Element of bool (bool [:NAT,REAL:])
bool (bool [:NAT,REAL:]) is non empty non trivial non finite set
the topology of (TOP-REAL 0) is non empty open Element of bool (bool the carrier of (TOP-REAL 0))
bool (bool the carrier of (TOP-REAL 0)) is non empty set
TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) is non empty strict TopSpace-like TopStruct
TM is TopSpace-like () TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is closed Element of bool the carrier of TM
TM | M is strict TopSpace-like SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
bool (bool the carrier of (TM | M)) is non empty set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
V1 is Element of bool (bool the carrier of (TM | M))
V2 is set
TMM is Element of bool the carrier of (TM | M)
the topology of (TM | M) is non empty open Element of bool (bool the carrier of (TM | M))
[#] (TM | M) is non proper open closed dense Element of bool the carrier of (TM | M)
mV1 is Element of bool the carrier of TM
mV1 /\ ([#] (TM | M)) is Element of bool the carrier of (TM | M)
mV1 /\ M is Element of bool the carrier of TM
[:V1, the topology of TM:] is Relation-like set
bool [:V1, the topology of TM:] is non empty set
V2 is Relation-like V1 -defined the topology of TM -valued Function-like V27(V1, the topology of TM) Element of bool [:V1, the topology of TM:]
M ` is open Element of bool the carrier of TM
the carrier of TM \ M is set
{(M `)} is non empty trivial finite 1 -element Element of bool (bool the carrier of TM)
rng V2 is Element of bool the topology of TM
bool the topology of TM is non empty set
TMM is open Element of bool (bool the carrier of TM)
mV1 is open Element of bool (bool the carrier of TM)
TMM \/ mV1 is Element of bool (bool the carrier of TM)
[#] (TM | M) is non proper open closed dense Element of bool the carrier of (TM | M)
dom V2 is Element of bool V1
bool V1 is non empty set
[#] TM is non proper open closed dense Element of bool the carrier of TM
mV2 is open Element of bool (bool the carrier of TM)
union mV2 is Element of bool the carrier of TM
M \/ (M `) is Element of bool the carrier of TM
[#] the carrier of TM is non proper Element of bool the carrier of TM
mL is set
union V1 is Element of bool the carrier of (TM | M)
U9 is set
V2 . U9 is set
(V2 . U9) /\ M is Element of bool the carrier of TM
mL is Element of bool (bool the carrier of TM)
mL | M is Element of bool (bool the carrier of (TM | M))
A1 is Element of bool (bool the carrier of (TM | M))
(mL | M) \ A1 is Element of bool (bool the carrier of (TM | M))
W9 is Element of bool (bool the carrier of (TM | M))
u is set
w is Element of bool the carrier of TM
w /\ M is Element of bool the carrier of TM
u1 is set
V2 . u1 is set
M \ M is Element of bool the carrier of TM
union mL is Element of bool the carrier of TM
union (mL | M) is Element of bool the carrier of (TM | M)
union W9 is Element of bool the carrier of (TM | M)
card (mL | M) is epsilon-transitive epsilon-connected ordinal cardinal set
card mL is epsilon-transitive epsilon-connected ordinal cardinal set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable separable metrizable () TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable separable metrizable () SubSpace of TM
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
TM is non empty Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr TM is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of TM is non empty set
Family_open_set TM is Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
TopStruct(# the carrier of TM,(Family_open_set TM) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr TM) is non empty set
bool the carrier of (TopSpaceMetr TM) is non empty set
A1 is non empty Element of bool the carrier of (TopSpaceMetr TM)
dist_min A1 is Relation-like the carrier of (TopSpaceMetr TM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TM), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:]
[: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:] is non empty set
A2 is non empty Element of bool the carrier of (TopSpaceMetr TM)
dist_min A2 is Relation-like the carrier of (TopSpaceMetr TM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TM), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:]
{ b1 where b1 is Element of the carrier of (TopSpaceMetr TM) : not 0 <= ((dist_min A1) . b1) - ((dist_min A2) . b1) } is set
TMM is Relation-like the carrier of (TopSpaceMetr TM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TM), the carrier of R^1) V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TM), the carrier of R^1:]
].-infty,0.[ is Element of bool REAL
mV2 is Element of bool the carrier of R^1
TMM " mV2 is Element of bool the carrier of (TopSpaceMetr TM)
mL is set
TMM . mL is V11() real ext-real set
U9 is Element of the carrier of (TopSpaceMetr TM)
(dist_min A1) . U9 is V11() real ext-real Element of the carrier of R^1
(dist_min A2) . U9 is V11() real ext-real Element of the carrier of R^1
((dist_min A1) . U9) - ((dist_min A2) . U9) is V11() real ext-real set
mL is set
U9 is Element of the carrier of (TopSpaceMetr TM)
(dist_min A1) . U9 is V11() real ext-real Element of the carrier of R^1
(dist_min A2) . U9 is V11() real ext-real Element of the carrier of R^1
((dist_min A1) . U9) - ((dist_min A2) . U9) is V11() real ext-real set
TMM . U9 is V11() real ext-real Element of the carrier of R^1
dom TMM is Element of bool the carrier of (TopSpaceMetr TM)
[#] (TopSpaceMetr TM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TM)
[#] R^1 is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of R^1
[#] (TopSpaceMetr TM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TM)
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
the topology of TM is non empty open Element of bool (bool the carrier of TM)
bool (bool the carrier of TM) is non empty set
[: the carrier of TM, the carrier of TM:] is Relation-like set
[:[: the carrier of TM, the carrier of TM:],REAL:] is Relation-like set
bool [:[: the carrier of TM, the carrier of TM:],REAL:] is non empty set
V2 is Relation-like [: the carrier of TM, the carrier of TM:] -defined REAL -valued Function-like V27([: the carrier of TM, the carrier of TM:], REAL ) V251() V252() V253() Element of bool [:[: the carrier of TM, the carrier of TM:],REAL:]
SpaceMetr ( the carrier of TM,V2) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of TM,V2)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of TM,V2)))
the carrier of (SpaceMetr ( the carrier of TM,V2)) is set
bool the carrier of (SpaceMetr ( the carrier of TM,V2)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of TM,V2))) is non empty set
{} TM is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable F_sigma G_delta boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of TM
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
{} TM is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable F_sigma G_delta boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of TM
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
{} TM is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable F_sigma G_delta boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of TM
TMM is non empty Reflexive discerning V210() triangle Discerning MetrStruct
TopSpaceMetr TMM is non empty strict TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of TMM is non empty set
Family_open_set TMM is Element of bool (bool the carrier of TMM)
bool the carrier of TMM is non empty set
bool (bool the carrier of TMM) is non empty set
TopStruct(# the carrier of TMM,(Family_open_set TMM) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr TMM) is non empty set
bool the carrier of (TopSpaceMetr TMM) is non empty set
mV2 is Element of bool the carrier of (TopSpaceMetr TMM)
dist_min mV2 is Relation-like the carrier of (TopSpaceMetr TMM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TMM), the carrier of R^1) V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TMM), the carrier of R^1:]
[: the carrier of (TopSpaceMetr TMM), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (TopSpaceMetr TMM), the carrier of R^1:] is non empty set
mL is Element of bool the carrier of (TopSpaceMetr TMM)
dist_min mL is Relation-like the carrier of (TopSpaceMetr TMM) -defined the carrier of R^1 -valued Function-like V27( the carrier of (TopSpaceMetr TMM), the carrier of R^1) V251() V252() V253() Element of bool [: the carrier of (TopSpaceMetr TMM), the carrier of R^1:]
{ b1 where b1 is Element of the carrier of TMM : not 0 <= ((dist_min mV2) . b1) - ((dist_min mL) . b1) } is set
{ b1 where b1 is Element of the carrier of TMM : not 0 <= ((dist_min mL) . b1) - ((dist_min mV2) . b1) } is set
u is open F_sigma Borel Element of bool the carrier of (TopSpaceMetr TMM)
w is open F_sigma Borel Element of bool the carrier of (TopSpaceMetr TMM)
u1 is open F_sigma Element of bool the carrier of TM
w1 is open F_sigma Element of bool the carrier of TM
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
[#] (TopSpaceMetr TMM) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr TMM)
U1 is set
Cl A1 is closed G_delta Element of bool the carrier of TM
Cl mL is closed G_delta Borel Element of bool the carrier of (TopSpaceMetr TMM)
W1 is Element of the carrier of TMM
(dist_min mL) . W1 is V11() real ext-real set
(dist_min mV2) . W1 is V11() real ext-real set
((dist_min mV2) . W1) - ((dist_min mL) . W1) is V11() real ext-real set
U1 is set
Cl M is closed G_delta Element of bool the carrier of TM
Cl mV2 is closed G_delta Borel Element of bool the carrier of (TopSpaceMetr TMM)
W1 is Element of the carrier of TMM
(dist_min mV2) . W1 is V11() real ext-real set
(dist_min mL) . W1 is V11() real ext-real set
((dist_min mL) . W1) - ((dist_min mV2) . W1) is V11() real ext-real set
U1 is set
W1 is Element of the carrier of TMM
(dist_min mL) . W1 is V11() real ext-real set
(dist_min mV2) . W1 is V11() real ext-real set
((dist_min mL) . W1) - ((dist_min mV2) . W1) is V11() real ext-real set
((dist_min mV2) . W1) - ((dist_min mL) . W1) is V11() real ext-real set
- (((dist_min mV2) . W1) - ((dist_min mL) . W1)) is V11() real ext-real set
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element ext-real non positive non negative countable V251() V252() V253() V254() set
L is Element of the carrier of TMM
(dist_min mV2) . L is V11() real ext-real set
(dist_min mL) . L is V11() real ext-real set
((dist_min mV2) . L) - ((dist_min mL) . L) is V11() real ext-real set
{} TM is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional finite finite-yielding V34() cardinal 0 -element open closed ext-real non positive non negative countable F_sigma G_delta boundary nowhere_dense V251() V252() V253() V254() Element of bool the carrier of TM
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
A2 is open F_sigma Element of bool the carrier of TM
V1 is open F_sigma Element of bool the carrier of TM
A2 \/ V1 is open F_sigma Element of bool the carrier of TM
(A2 \/ V1) ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ (A2 \/ V1) is set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
M is Element of bool the carrier of TM
TM | M is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
the carrier of (TM | M) is set
bool the carrier of (TM | M) is non empty set
A1 is closed G_delta Element of bool the carrier of TM
A2 is closed G_delta Element of bool the carrier of TM
V1 is open F_sigma Element of bool the carrier of TM
V2 is open F_sigma Element of bool the carrier of TM
Cl V1 is closed G_delta Element of bool the carrier of TM
Cl V2 is closed G_delta Element of bool the carrier of TM
M /\ (Cl V1) is Element of bool the carrier of TM
M /\ (Cl V2) is Element of bool the carrier of TM
mV1 is Element of bool the carrier of (TM | M)
mV2 is Element of bool the carrier of (TM | M)
mL is Element of bool the carrier of (TM | M)
V2 /\ M is Element of bool the carrier of TM
U9 is open F_sigma Element of bool the carrier of (TM | M)
W9 is open F_sigma Element of bool the carrier of (TM | M)
U9 \/ W9 is open F_sigma Element of bool the carrier of (TM | M)
(U9 \/ W9) ` is closed G_delta Element of bool the carrier of (TM | M)
the carrier of (TM | M) \ (U9 \/ W9) is set
[#] (TM | M) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (TM | M)
u is Element of bool the carrier of TM
u \/ A1 is Element of bool the carrier of TM
w is Element of bool the carrier of TM
w \/ A2 is Element of bool the carrier of TM
mV2 /\ u is Element of bool the carrier of TM
U9 /\ W9 is open F_sigma Element of bool the carrier of (TM | M)
V2 /\ u is Element of bool the carrier of TM
M /\ u is Element of bool the carrier of TM
V2 /\ (M /\ u) is Element of bool the carrier of TM
(V2 /\ M) /\ u is Element of bool the carrier of TM
Cl u is closed G_delta Element of bool the carrier of TM
Cl (u \/ A1) is closed G_delta Element of bool the carrier of TM
U1 is set
Cl A1 is closed G_delta Element of bool the carrier of TM
(Cl u) \/ (Cl A1) is closed G_delta Element of bool the carrier of TM
V1 /\ M is Element of bool the carrier of TM
mV1 /\ w is Element of bool the carrier of TM
V1 /\ w is Element of bool the carrier of TM
M /\ w is Element of bool the carrier of TM
V1 /\ (M /\ w) is Element of bool the carrier of TM
(V1 /\ M) /\ w is Element of bool the carrier of TM
Cl w is closed G_delta Element of bool the carrier of TM
Cl (w \/ A2) is closed G_delta Element of bool the carrier of TM
U1 is set
Cl A2 is closed G_delta Element of bool the carrier of TM
(Cl w) \/ (Cl A2) is closed G_delta Element of bool the carrier of TM
U1 is open F_sigma Element of bool the carrier of TM
W1 is open F_sigma Element of bool the carrier of TM
U1 \/ W1 is open F_sigma Element of bool the carrier of TM
(U1 \/ W1) ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ (U1 \/ W1) is set
L is closed G_delta Element of bool the carrier of TM
M /\ L is Element of bool the carrier of TM
u \/ w is Element of bool the carrier of TM
([#] (TM | M)) \ (U9 \/ W9) is Element of bool the carrier of (TM | M)
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
M /\ ([#] TM) is Element of bool the carrier of TM
(M /\ ([#] TM)) \ (U1 \/ W1) is Element of bool the carrier of TM
M \ (U1 \/ W1) is Element of bool the carrier of TM
M \ (U9 \/ W9) is Element of bool the carrier of TM