:: METRIZTS semantic presentation

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

{ H

card { H

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

{ [:b

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

{ H

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 { H

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

{ H

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 { H

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

{ b

].-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

{ b

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

{ b

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

{ b

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

{ b

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

{ H