:: METRIZTS semantic presentation

REAL is non trivial non finite non countable set

bool REAL is non empty non trivial non finite set

bool omega is non empty non trivial non finite set
is non trivial Relation-like non finite set
bool is non empty non trivial non finite set
bool () is non empty non trivial non finite set

{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

bool is non empty set

[: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

INT is set
bool 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 () is non empty set
K585() is non empty strict TopSpace-like V316() TopStruct
the carrier of K585() is non empty V263() set

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

is non empty trivial functional finite V34() 1 -element set
meet 0 is set

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, #) 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

the carrier of TM is set
bool the carrier of TM is non empty set

the carrier of M is set
bool the carrier of M is non empty 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

bool the carrier of M is non empty finite V34() set

bool the carrier of TM is non empty finite V34() set

[: 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

[#] 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 | ([#] 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

the carrier of TM is set
bool the carrier of TM is non empty set

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))

the carrier of TM is set
bool the carrier of TM is non empty set

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

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)

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)

bool the carrier of TM is non empty finite V34() set
bool (bool the carrier of TM) is non empty finite V34() set

the topology of TM is non empty finite V34() open Element of bool (bool the carrier of TM)

A1 is finite V34() V65(TM) open Element of bool (bool the carrier of TM)

[#] 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

the carrier of TM is set

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

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 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)):]

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,() #) is strict TopStruct

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 () is set
bool the carrier of () is non empty set
[#] () is non proper open closed dense Element of bool the carrier of ()
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 (), the carrier of ():] is Relation-like set
[:[: the carrier of (), the carrier of ():],REAL:] is Relation-like set
bool [:[: the carrier of (), the carrier of ():],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 (), the carrier of ():] -defined REAL -valued Function-like V27([: the carrier of (), the carrier of ():], REAL ) V251() V252() V253() Element of bool [:[: the carrier of (), the carrier of ():],REAL:]
SpaceMetr ( the carrier of (),TMM) is strict Reflexive discerning V210() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of (),TMM)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of (),TMM)))
the carrier of (SpaceMetr ( the carrier of (),TMM)) is set
bool the carrier of (SpaceMetr ( the carrier of (),TMM)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of (),TMM))) is non empty set
the topology of () is non empty open Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
V1 is Element of bool the carrier of ()
() | 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

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

the carrier of A2 is non empty set
bool the carrier of A2 is non empty set

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,() #) is non empty strict TopStruct
the carrier of () is non empty set
bool the carrier of () 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 ()
() | 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

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
[#] (() | 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

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

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,() #) 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

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,() #) 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

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)

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)

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 V2),(card TMM):] is non empty Relation-like set
card [:(card V2),(card TMM):] is non empty 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

mV1 is V65(TMM) open Element of bool (bool the carrier of TMM)

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

mL is V65(TM) open Element of bool (bool the carrier of TM)

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)

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

[#] (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

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)

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

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))
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 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,() #) is non empty strict TopStruct
the carrier of () is non empty set
bool the carrier of () is non empty set
M is non empty Element of bool the carrier of ()
dist_min M is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V27( the carrier of (), the carrier of R^1) V251() V252() V253() Element of bool [: the carrier of (), the carrier of R^1:]
[: the carrier of (), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (), the carrier of R^1:] is non empty set
V1 is Element of bool the carrier of R^1
() " V1 is Element of bool the carrier of ()
the carrier of is non empty set
bool the carrier of is non empty set
TMM is Element of the carrier of TM
() . TMM is V11() real ext-real set
mV1 is Element of the carrier of RealSpace
V2 is open Element of bool the carrier of
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 () is Element of bool the carrier of ()
[#] TM is non empty non proper Element of bool the carrier of TM
() . U9 is V11() real ext-real set
rng () 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)) + (() . TMM) is V11() real ext-real set
(() . U9) - (() . TMM) is V11() real ext-real set
- (dist (TMM,U9)) is V11() real ext-real set
- ((() . U9) - (() . TMM)) is V11() real ext-real set
(dist (TMM,U9)) + (() . U9) is V11() real ext-real set
(() . TMM) - (() . U9) is V11() real ext-real set
abs ((() . TMM) - (() . 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
[#] () is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of ()

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

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,() #) is non empty strict TopStruct
the carrier of () is non empty set
bool the carrier of () is non empty set
A1 is non empty Element of bool the carrier of ()
dist_min A1 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V27( the carrier of (), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (), the carrier of R^1:]
[: the carrier of (), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (), 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 () : 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 ()
mV1 is set
mV2 is Element of the carrier of ()
(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 ()
[#] () is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of ()
mV1 is set
mV2 is Element of the carrier of ()
(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
[#] () is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of ()

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

[#] 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

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,() #) is non empty strict TopStruct
the topology of () is non empty open Element of bool (bool the carrier of ())
the carrier of () is non empty set
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set

({} ()) ` is open closed dense Element of bool the carrier of ()
the carrier of () \ ({} ()) is set
[#] () is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of ()
mV1 is open Element of bool the carrier of ()
mV1 ` is closed Element of bool the carrier of ()
the carrier of () \ mV1 is set
mV2 is non empty closed Element of bool the carrier of ()
dist_min mV2 is Relation-like the carrier of () -defined the carrier of R^1 -valued Function-like V27( the carrier of (), the carrier of R^1) continuous V251() V252() V253() Element of bool [: the carrier of (), the carrier of R^1:]
[: the carrier of (), the carrier of R^1:] is non empty Relation-like V251() V252() V253() set
bool [: the carrier of (), the carrier of R^1:] is non empty set
mL is set

1 / (2 |^ U9) is V11() real ext-real set
{ b1 where b1 is Element of the carrier of () : not 1 / (2 |^ U9) <= (dist_min mV2) . b1 } is set
W9 is open Element of bool the carrier of ()

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 () : 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 () 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

(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 () : not 1 / (2 |^ U1) <= (dist_min mV2) . b1 } is set
u is set
Cl mV2 is closed Element of bool the carrier of ()
w is Element of the carrier of ()
(dist_min mV2) . w is V11() real ext-real Element of the carrier of R^1

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 () : not 1 / (2 |^ u1) <= (dist_min mV2) . b1 } is set
U1 is Element of the carrier of ()
(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

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

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

(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

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

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

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