:: WEIERSTR semantic presentation

REAL is non empty non trivial V47() V48() V49() V53() non finite set

NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K6(REAL)

K6(REAL) is non empty set

COMPLEX is non empty non trivial V47() V53() non finite set

RAT is non empty non trivial V47() V48() V49() V50() V53() non finite set

INT is non empty non trivial V47() V48() V49() V50() V51() V53() non finite set

omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() set

K6(omega) is non empty set

K6(NAT) is non empty set

K7(COMPLEX,COMPLEX) is non empty set

K6(K7(COMPLEX,COMPLEX)) is non empty set

K7(COMPLEX,REAL) is non empty set

K6(K7(COMPLEX,REAL)) is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

K7(1,1) is non empty set

K6(K7(1,1)) is non empty set

K7(K7(1,1),1) is non empty set

K6(K7(K7(1,1),1)) is non empty set

K7(K7(1,1),REAL) is non empty set

K6(K7(K7(1,1),REAL)) is non empty set

K7(REAL,REAL) is non empty set

K7(K7(REAL,REAL),REAL) is non empty set

K6(K7(K7(REAL,REAL),REAL)) is non empty set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

K7(2,2) is non empty set

K7(K7(2,2),REAL) is non empty set

K6(K7(K7(2,2),REAL)) is non empty set

K6(K7(REAL,REAL)) is non empty set

TOP-REAL 2 is non empty TopSpace-like V139() V164() V165() V166() V167() V168() V169() V170() V176() L15()

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

K452() is V200() TopStruct

the carrier of K452() is V47() V48() V49() set

RealSpace is non empty strict Reflexive discerning V122() triangle Discerning V200() MetrStruct

R^1 is non empty strict TopSpace-like V200() TopStruct

K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K7(RAT,RAT) is non empty set

K6(K7(RAT,RAT)) is non empty set

K7(K7(RAT,RAT),RAT) is non empty set

K6(K7(K7(RAT,RAT),RAT)) is non empty set

K7(INT,INT) is non empty set

K6(K7(INT,INT)) is non empty set

K7(K7(INT,INT),INT) is non empty set

K6(K7(K7(INT,INT),INT)) is non empty set

K7(NAT,NAT) is non empty set

K7(K7(NAT,NAT),NAT) is non empty set

K6(K7(K7(NAT,NAT),NAT)) is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real functional V47() V48() V49() V50() V51() V52() V53() finite V58() FinSequence-membered set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

union {} is epsilon-transitive epsilon-connected ordinal finite set

K7(NAT,REAL) is non empty set

K6(K7(NAT,REAL)) is non empty set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real functional V45() V46() V47() V48() V49() V50() V51() V52() V53() finite V58() FinSequence-membered Element of NAT

the carrier of RealSpace is non empty V47() V48() V49() set

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

the carrier of R^1 is non empty V47() V48() V49() set

real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V30(K7(REAL,REAL), REAL ) Element of K6(K7(K7(REAL,REAL),REAL))

MetrStruct(# REAL,real_dist #) is strict MetrStruct

M is Reflexive discerning V122() triangle MetrStruct

the carrier of M is set

P is Element of the carrier of M

Q is Element of the carrier of M

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

Ball (P,x1) is Element of K6( the carrier of M)

K6( the carrier of M) is non empty set

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

Ball (Q,x2) is Element of K6( the carrier of M)

(Ball (P,x1)) \/ (Ball (Q,x2)) is Element of K6( the carrier of M)

abs x1 is V11() real ext-real Element of REAL

abs x2 is V11() real ext-real Element of REAL

(abs x1) + (abs x2) is V11() real ext-real Element of REAL

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

((abs x1) + (abs x2)) + (dist (P,Q)) is V11() real ext-real Element of REAL

z is Element of the carrier of M

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

Ball (z,y) is Element of K6( the carrier of M)

c

z is Element of the carrier of M

x1 + 0 is V11() real ext-real Element of REAL

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

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

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

0 + y is V11() real ext-real Element of REAL

((dist (z,z)) - y) + y is V11() real ext-real Element of REAL

z is Element of the carrier of M

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

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

(dist (Q,z)) - (abs x2) is V11() real ext-real Element of REAL

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

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

0 + (abs x2) is V11() real ext-real Element of REAL

((dist (Q,z)) - (abs x2)) + (abs x2) is V11() real ext-real Element of REAL

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

(dist (z,z)) - (abs x2) is V11() real ext-real Element of REAL

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

((dist (z,z)) - (abs x2)) - (abs x1) is V11() real ext-real Element of REAL

(dist (z,z)) - ((abs x1) + (abs x2)) is V11() real ext-real Element of REAL

((dist (z,z)) - ((abs x1) + (abs x2))) + ((abs x1) + (abs x2)) is V11() real ext-real Element of REAL

z is Element of the carrier of M

z is Element of the carrier of M

M is Reflexive discerning V122() triangle MetrStruct

the carrier of M is set

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

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

P + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

Seg (P + 1) is V47() V48() V49() V50() V51() V52() finite V71(P + 1) Element of K6(NAT)

Seg P is V47() V48() V49() V50() V51() V52() finite V71(P) Element of K6(NAT)

Q is Element of K6(K6( the carrier of M))

union Q is Element of K6( the carrier of M)

x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng x1 is finite set

dom x1 is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

x1 . (P + 1) is set

x2 is Element of the carrier of M

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

Ball (x2,z) is Element of K6( the carrier of M)

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

Ball (x2,z) is Element of K6( the carrier of M)

x1 | (Seg P) is Relation-like finite FinSubsequence-like set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

c

len x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

{(P + 1)} is non empty V47() V48() V49() V50() V51() V52() finite Element of K6(REAL)

(dom y) \/ {(P + 1)} is non empty V47() V48() V49() V50() V51() V52() finite set

z is Element of K6(K6( the carrier of M))

union z is Element of K6( the carrier of M)

(union z) \/ (Ball (x2,z)) is Element of K6( the carrier of M)

z is set

q is set

y is set

x1 . y is set

y . y is set

z is set

z is Element of the carrier of M

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

Ball (z,q) is Element of K6( the carrier of M)

(union z) \/ (Ball (z,q)) is Element of K6( the carrier of M)

M is Reflexive discerning V122() triangle MetrStruct

the carrier of M is set

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

P is Element of K6(K6( the carrier of M))

union P is Element of K6( the carrier of M)

Q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng Q is finite set

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

x1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

x2 is Element of K6(K6( the carrier of M))

union x2 is Element of K6( the carrier of M)

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

Seg z is V47() V48() V49() V50() V51() V52() finite V71(z) Element of K6(NAT)

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

Seg x1 is V47() V48() V49() V50() V51() V52() finite V71(x1) Element of K6(NAT)

c

union c

z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng z is finite set

dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

z is Element of the carrier of M

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

Ball (z,q) is Element of K6( the carrier of M)

(union c

z is Element of the carrier of M

z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng z is finite set

dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

q is Element of the carrier of M

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

Ball (q,y) is Element of K6( the carrier of M)

(union c

z is Element of the carrier of M

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

Ball (z,q) is Element of K6( the carrier of M)

(union c

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

Ball (z,q) is Element of K6( the carrier of M)

(union c

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

Ball (z,y) is Element of K6( the carrier of M)

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

Ball (z,y) is Element of K6( the carrier of M)

(Ball (z,y)) \/ (Ball (z,q)) is Element of K6( the carrier of M)

G is Element of the carrier of M

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

Ball (G,G) is Element of K6( the carrier of M)

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

Ball (G,G) is Element of K6( the carrier of M)

x1 is Element of K6(K6( the carrier of M))

union x1 is Element of K6( the carrier of M)

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

Seg x2 is V47() V48() V49() V50() V51() V52() finite V71(x2) Element of K6(NAT)

the Element of the carrier of M is Element of the carrier of M

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

dom y is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

Ball ( the Element of the carrier of M,0) is Element of K6( the carrier of M)

z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng z is finite set

dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

x1 is Element of K6(K6( the carrier of M))

z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng z is finite set

dom z is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

Seg x2 is V47() V48() V49() V50() V51() V52() finite V71(x2) Element of K6(NAT)

union x1 is Element of K6( the carrier of M)

dom Q is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

Seg x1 is V47() V48() V49() V50() V51() V52() finite V71(x1) Element of K6(NAT)

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

K7( the carrier of M, the carrier of P) is non empty set

K6(K7( the carrier of M, the carrier of P)) is non empty set

K6( the carrier of P) is non empty set

K6(K6( the carrier of P)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))

x1 is Element of K6(K6( the carrier of P))

Q " x1 is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

x2 is Element of K6( the carrier of M)

z is Element of K6( the carrier of P)

Q " z is Element of K6( the carrier of M)

[#] P is non empty non proper Element of K6( the carrier of P)

y is Element of K6( the carrier of P)

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

K7( the carrier of M, the carrier of P) is non empty set

K6(K7( the carrier of M, the carrier of P)) is non empty set

K6( the carrier of P) is non empty set

K6(K6( the carrier of P)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))

x1 is Element of K6(K6( the carrier of P))

Q " x1 is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

[#] P is non empty non proper Element of K6( the carrier of P)

K6(([#] P)) is non empty set

[#] M is non empty non proper Element of K6( the carrier of M)

K6(([#] M)) is non empty set

x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng x2 is finite set

z is Element of K6(([#] P))

y is set

Q " y is Element of K6( the carrier of M)

z is Element of K6(([#] M))

z is set

q is set

Q " z is Element of K6( the carrier of M)

bool ([#] P) is non empty Element of K6(K6(([#] P)))

K6(K6(([#] P))) is non empty set

bool ([#] M) is non empty Element of K6(K6(([#] M)))

K6(K6(([#] M))) is non empty set

K7((bool ([#] P)),(bool ([#] M))) is non empty set

K6(K7((bool ([#] P)),(bool ([#] M)))) is non empty set

z is Relation-like bool ([#] P) -defined bool ([#] M) -valued Function-like V30( bool ([#] P), bool ([#] M)) Element of K6(K7((bool ([#] P)),(bool ([#] M))))

dom z is Element of K6((bool ([#] P)))

K6((bool ([#] P))) is non empty set

x2 * z is Relation-like finite set

z .: x1 is Element of K6((bool ([#] M)))

K6((bool ([#] M))) is non empty set

c

z is set

z . z is set

z is Element of K6( the carrier of P)

z . z is set

Q " z is Element of K6( the carrier of M)

z is Element of K6( the carrier of M)

z is Element of K6( the carrier of P)

Q " z is Element of K6( the carrier of M)

z . z is set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

c

rng c

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

K7( the carrier of M, the carrier of P) is non empty set

K6(K7( the carrier of M, the carrier of P)) is non empty set

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))

x1 is Element of K6(K6( the carrier of M))

Q .: x1 is Element of K6(K6( the carrier of P))

K6( the carrier of P) is non empty set

K6(K6( the carrier of P)) is non empty set

[#] M is non empty non proper Element of K6( the carrier of M)

K6(([#] M)) is non empty set

[#] P is non empty non proper Element of K6( the carrier of P)

K6(([#] P)) is non empty set

x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng x2 is finite set

z is Element of K6(([#] M))

y is set

Q .: y is Element of K6( the carrier of P)

z is Element of K6(([#] P))

z is set

q is set

Q .: z is Element of K6( the carrier of P)

bool ([#] M) is non empty Element of K6(K6(([#] M)))

K6(K6(([#] M))) is non empty set

bool ([#] P) is non empty Element of K6(K6(([#] P)))

K6(K6(([#] P))) is non empty set

K7((bool ([#] M)),(bool ([#] P))) is non empty set

K6(K7((bool ([#] M)),(bool ([#] P)))) is non empty set

z is Relation-like bool ([#] M) -defined bool ([#] P) -valued Function-like V30( bool ([#] M), bool ([#] P)) Element of K6(K7((bool ([#] M)),(bool ([#] P))))

dom z is Element of K6((bool ([#] M)))

K6((bool ([#] M))) is non empty set

x2 * z is Relation-like finite set

z .: x1 is Element of K6((bool ([#] P)))

K6((bool ([#] P))) is non empty set

c

z is set

z . z is set

z is Element of K6( the carrier of M)

z . z is set

Q .: z is Element of K6( the carrier of P)

z is Element of K6( the carrier of P)

z is Element of K6( the carrier of M)

Q .: z is Element of K6( the carrier of P)

z . z is set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

c

rng c

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

K7( the carrier of M, the carrier of P) is non empty set

K6(K7( the carrier of M, the carrier of P)) is non empty set

K6( the carrier of M) is non empty set

K6( the carrier of P) is non empty set

K6(K6( the carrier of P)) is non empty set

K6(K6( the carrier of M)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))

x1 is Element of K6( the carrier of M)

Q .: x1 is Element of K6( the carrier of P)

x2 is Element of K6(K6( the carrier of P))

Q " x2 is Element of K6(K6( the carrier of M))

z is Element of K6(K6( the carrier of M))

union z is Element of K6( the carrier of M)

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng y is finite set

c

[#] P is non empty non proper Element of K6( the carrier of P)

K6(([#] P)) is non empty set

z is Element of c

z is Element of K6( the carrier of M)

q is Element of K6( the carrier of P)

Q " q is Element of K6( the carrier of M)

y is Element of K6(([#] P))

G is Element of c

G is Element of K6(([#] P))

Q " G is Element of K6( the carrier of M)

bool ([#] P) is non empty Element of K6(K6(([#] P)))

K6(K6(([#] P))) is non empty set

K7(c

K6(K7(c

z is Relation-like c

z is Element of c

z . z is Element of bool ([#] P)

q is Element of c

z . q is Element of bool ([#] P)

Q " (z . q) is Element of K6( the carrier of M)

K7(z,(bool ([#] P))) is set

K6(K7(z,(bool ([#] P)))) is non empty set

z is Relation-like z -defined bool ([#] P) -valued Function-like V30(z, bool ([#] P)) Element of K6(K7(z,(bool ([#] P))))

dom z is Element of K6(z)

K6(z) is non empty set

y * z is Relation-like finite set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

G is set

dom q is V47() V48() V49() V50() V51() V52() finite Element of K6(NAT)

G is set

q . G is set

y . G is set

z . (y . G) is set

G is Element of K6(K6( the carrier of P))

G is Element of K6(K6( the carrier of P))

union G is Element of K6( the carrier of P)

x is set

dom Q is Element of K6( the carrier of M)

y is set

Q . y is set

C is set

z . C is set

Q " (z . C) is Element of K6( the carrier of M)

Q .: (Q " (z . C)) is Element of K6( the carrier of P)

rng z is Element of K6((bool ([#] P)))

K6((bool ([#] P))) is non empty set

y is set

y is Element of K6(K6( the carrier of P))

c

z is Element of K6(K6( the carrier of P))

z is set

dom Q is Element of K6( the carrier of M)

q is set

Q . q is set

y is Element of K6(K6( the carrier of P))

y is Element of K6(K6( the carrier of P))

c

z is Element of K6(K6( the carrier of P))

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

K7( the carrier of M, the carrier of P) is non empty set

K6(K7( the carrier of M, the carrier of P)) is non empty set

K6( the carrier of M) is non empty set

Q is Relation-like the carrier of M -defined the carrier of P -valued Function-like V30( the carrier of M, the carrier of P) Element of K6(K7( the carrier of M, the carrier of P))

x1 is Element of K6( the carrier of M)

Q .: x1 is Element of K6( the carrier of P)

K6( the carrier of P) is non empty set

[#] M is non empty non proper Element of K6( the carrier of M)

dom Q is Element of K6( the carrier of M)

K6(K6( the carrier of P)) is non empty set

x2 is Element of K6(K6( the carrier of P))

Q " x2 is Element of K6(K6( the carrier of M))

K6(K6( the carrier of M)) is non empty set

union x2 is Element of K6( the carrier of P)

union (Q " x2) is Element of K6( the carrier of M)

y is set

Q " (union x2) is Element of K6( the carrier of M)

c

Q . c

z is set

Q " z is Element of K6( the carrier of M)

z is set

Q . y is set

c

Q . c

{(Q . c

Q " {(Q . c

z is set

Q . z is set

y is Element of K6(K6( the carrier of M))

y is Element of K6(K6( the carrier of P))

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

K6( the carrier of M) is non empty set

Q is Element of K6( the carrier of M)

P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

K6( the carrier of R^1) is non empty set

K7( the carrier of (TOP-REAL 2), the carrier of R^1) is non empty set

K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is non empty set

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

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

M is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

M .: P is V47() V48() V49() Element of K6( the carrier of R^1)

K6( the carrier of R^1) is non empty set

K6( the carrier of R^1) is non empty set

M is V47() V48() V49() Element of K6( the carrier of R^1)

M is V47() V48() V49() Element of K6( the carrier of R^1)

(M) is V47() V48() V49() Element of K6(REAL)

K6(K6( the carrier of R^1)) is non empty set

Q is Element of K6(K6( the carrier of R^1))

union Q is V47() V48() V49() Element of K6( the carrier of R^1)

x1 is set

K6( the carrier of RealSpace) is non empty set

x2 is V11() real ext-real Element of the carrier of RealSpace

Ball (x2,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)

z is V47() V48() V49() Element of K6( the carrier of RealSpace)

Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))

K6(K6( the carrier of RealSpace)) is non empty set

TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct

y is V47() V48() V49() Element of K6( the carrier of R^1)

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

c

x1 is V47() V48() V49() Element of K6( the carrier of R^1)

x2 is V11() real ext-real Element of the carrier of RealSpace

Ball (x2,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is non empty set

x1 is Element of K6(K6( the carrier of R^1))

union x1 is V47() V48() V49() Element of K6( the carrier of R^1)

x2 is set

z is V47() V48() V49() Element of K6( the carrier of R^1)

y is V11() real ext-real Element of the carrier of RealSpace

Ball (y,1) is V47() V48() V49() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is non empty set

Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))

K6( the carrier of RealSpace) is non empty set

K6(K6( the carrier of RealSpace)) is non empty set

TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct

x2 is Element of K6(K6( the carrier of RealSpace))

union x2 is V47() V48() V49() Element of K6( the carrier of RealSpace)

z is V11() real ext-real Element of the carrier of RealSpace

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

Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)

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

Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)

c

c

c

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

z is V11() real ext-real Element of the carrier of RealSpace

q is V11() real ext-real Element of the carrier of RealSpace

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

c

abs (c

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

(- y) + z is V11() real ext-real Element of REAL

c

z + y is V11() real ext-real Element of REAL

z is ext-real set

z is ext-real set

P is ext-real set

P is ext-real set

M is V47() V48() V49() Element of K6( the carrier of R^1)

(M) is V47() V48() V49() Element of K6(REAL)

P is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))

rng P is V47() V48() V49() Element of K6(REAL)

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

x1 is V11() real ext-real Element of the carrier of R^1

M ` is V47() V48() V49() Element of K6( the carrier of R^1)

x2 is V47() V48() V49() Element of K6( the carrier of R^1)

z is V47() V48() V49() Element of K6( the carrier of R^1)

Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))

K6( the carrier of RealSpace) is non empty set

K6(K6( the carrier of RealSpace)) is non empty set

TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct

y is V11() real ext-real Element of the carrier of RealSpace

c

Ball (y,c

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

Ball (y,z) is V47() V48() V49() Element of K6( the carrier of RealSpace)

{ b

z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

z + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() Element of NAT

P . (z + 1) is V11() real ext-real Element of REAL

(P . (z + 1)) - (lim P) is V11() real ext-real Element of REAL

abs ((P . (z + 1)) - (lim P)) is V11() real ext-real Element of REAL

real_dist . ((P . (z + 1)),(lim P)) is V11() real ext-real Element of REAL

real_dist . ((lim P),(P . (z + 1))) is V11() real ext-real Element of REAL

y is V11() real ext-real Element of the carrier of RealSpace

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

the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V30(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))

K7( the carrier of RealSpace, the carrier of RealSpace) is non empty set

K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is non empty set

K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is non empty set

the distance of RealSpace . (y,y) is V11() real ext-real Element of REAL

(Ball (y,z)) /\ (rng P) is V47() V48() V49() Element of K6(REAL)

P is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))

rng P is V47() V48() V49() Element of K6(REAL)

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

Q is set

M is V47() V48() V49() Element of K6( the carrier of R^1)

(M) is V47() V48() V49() Element of K6(REAL)

P is set

Q is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) Element of K6(K7(NAT,REAL))

rng Q is V47() V48() V49() Element of K6(REAL)

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

K6( the carrier of M) is non empty set

P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

Q is Element of K6( the carrier of M)

P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

((P .: Q)) is V47() V48() V49() Element of K6(REAL)

upper_bound ((P .: Q)) is V11() real ext-real Element of REAL

lower_bound ((P .: Q)) is V11() real ext-real Element of REAL

x1 is set

dom P is Element of K6( the carrier of M)

P . x1 is set

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

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

dom P is Element of K6( the carrier of M)

z is set

P . z is set

y is set

P . y is set

c

P . c

z is Element of the carrier of M

P . z is V11() real ext-real Element of the carrier of R^1

M is V47() V48() V49() Element of K6( the carrier of R^1)

(M) is V47() V48() V49() Element of K6(REAL)

upper_bound (M) is V11() real ext-real Element of REAL

lower_bound (M) is V11() real ext-real Element of REAL

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

K6( the carrier of M) is non empty set

P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

Q is Element of K6( the carrier of M)

P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

((P .: Q)) is V11() real ext-real Element of REAL

((P .: Q)) is V47() V48() V49() Element of K6(REAL)

upper_bound ((P .: Q)) is V11() real ext-real Element of REAL

lower_bound ((P .: Q)) is V11() real ext-real Element of REAL

x1 is Element of the carrier of M

x2 is Element of the carrier of M

P . x1 is V11() real ext-real Element of the carrier of R^1

P . x2 is V11() real ext-real Element of the carrier of R^1

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

K6( the carrier of M) is non empty set

P is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

Q is Element of K6( the carrier of M)

P .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

((P .: Q)) is V11() real ext-real Element of REAL

((P .: Q)) is V47() V48() V49() Element of K6(REAL)

lower_bound ((P .: Q)) is V11() real ext-real Element of REAL

upper_bound ((P .: Q)) is V11() real ext-real Element of REAL

x1 is Element of the carrier of M

x2 is Element of the carrier of M

P . x1 is V11() real ext-real Element of the carrier of R^1

P . x2 is V11() real ext-real Element of the carrier of R^1

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of M is non empty set

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

P is Element of the carrier of M

Q is Element of the carrier of M

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

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

x2 is V11() real ext-real Element of the carrier of R^1

z is Element of the carrier of M

y is V11() real ext-real Element of the carrier of R^1

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

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

x1 is Element of the carrier of M

Q . x1 is V11() real ext-real Element of the carrier of R^1

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

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is Element of the carrier of M

x1 . x2 is set

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

Q is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is set

Q . x2 is set

x1 . x2 is set

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

z is Element of the carrier of M

Q . z is set

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

x1 . z is set

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of M is non empty set

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

P is Element of the carrier of M

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

the carrier of (TopSpaceMetr M) is non empty set

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

Q is V47() V48() V49() Element of K6( the carrier of R^1)

(M,P) " Q is Element of K6( the carrier of (TopSpaceMetr M))

K6( the carrier of (TopSpaceMetr M)) is non empty set

x1 is Element of the carrier of M

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

x2 is V11() real ext-real Element of the carrier of RealSpace

(M,P) . x1 is set

the carrier of (TopSpaceMetr RealSpace) is non empty set

K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set

z is Element of K6( the carrier of (TopSpaceMetr RealSpace))

y is V11() real ext-real set

Ball (x2,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is non empty set

c

Ball (x1,c

K6( the carrier of M) is non empty set

(M,P) " z is Element of K6( the carrier of (TopSpaceMetr M))

z is set

z is Element of the carrier of M

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

q is V11() real ext-real Element of the carrier of RealSpace

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

c

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

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

(abs ((dist (x1,P)) - (dist (z,P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL

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

Ball (x2,c

(M,P) . z is set

dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))

[#] R^1 is non empty non proper V47() V48() V49() Element of K6( the carrier of R^1)

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of M is non empty set

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

Q is Element of K6( the carrier of (TopSpaceMetr M))

P is Element of the carrier of M

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,P) .: Q)) is V11() real ext-real Element of REAL

(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of M is non empty set

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

Q is Element of K6( the carrier of (TopSpaceMetr M))

P is Element of the carrier of M

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,P) .: Q)) is V11() real ext-real Element of REAL

(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of the carrier of M

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

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

x2 is V11() real ext-real Element of the carrier of R^1

z is Element of the carrier of M

y is V11() real ext-real Element of the carrier of R^1

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

x1 is Element of the carrier of M

Q . x1 is V11() real ext-real Element of the carrier of R^1

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is Element of the carrier of M

x1 . x2 is set

(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x2) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x2) .: P)) is V11() real ext-real Element of REAL

(((M,x2) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x2) .: P)) is V11() real ext-real Element of REAL

Q is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is set

Q . x2 is set

x1 . x2 is set

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

z is Element of the carrier of M

Q . z is set

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

x1 . z is set

Q is Element of the carrier of M

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

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

x2 is V11() real ext-real Element of the carrier of R^1

z is Element of the carrier of M

y is V11() real ext-real Element of the carrier of R^1

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

K7( the carrier of M, the carrier of R^1) is non empty set

K6(K7( the carrier of M, the carrier of R^1)) is non empty set

Q is Relation-like the carrier of M -defined the carrier of R^1 -valued Function-like V30( the carrier of M, the carrier of R^1) Element of K6(K7( the carrier of M, the carrier of R^1))

x1 is Element of the carrier of M

Q . x1 is V11() real ext-real Element of the carrier of R^1

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is Element of the carrier of M

x1 . x2 is set

(M,x2) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x2) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x2) .: P)) is V11() real ext-real Element of REAL

(((M,x2) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,x2) .: P)) is V11() real ext-real Element of REAL

Q is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x1 is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

x2 is set

Q . x2 is set

x1 . x2 is set

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

z is Element of the carrier of M

Q . z is set

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

x1 . z is set

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of the carrier of M

x1 is Element of the carrier of M

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

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V11() real ext-real Element of REAL

lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

(M,x1) . Q is set

dom (M,x1) is Element of K6( the carrier of (TopSpaceMetr M))

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of the carrier of M

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

x1 is Element of the carrier of M

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) - (((M,x1) .: P)) is V11() real ext-real Element of REAL

abs ((((M,Q) .: P)) - (((M,x1) .: P))) is V11() real ext-real Element of REAL

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

x2 is Element of the carrier of (TopSpaceMetr M)

(M,Q) . x2 is V11() real ext-real Element of the carrier of R^1

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

y is Element of the carrier of (TopSpaceMetr M)

(M,x1) . y is V11() real ext-real Element of the carrier of R^1

c

dist (c

z is Element of the carrier of M

(M,Q) . z is set

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

dist (c

(dist (c

(dist (c

((dist (c

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

- ((dist (c

(M,x1) . c

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

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

(dist (z,x1)) + (dist (x1,Q)) is V11() real ext-real Element of REAL

(dist (z,Q)) - (dist (c

(dist (z,x1)) + (dist (Q,x1)) is V11() real ext-real Element of REAL

((dist (z,x1)) + (dist (Q,x1))) - (dist (z,x1)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

Q is Element of the carrier of M

(M,P) . Q is set

x1 is Element of the carrier of M

(M,P) . x1 is set

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

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

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

x2 - z is V11() real ext-real Element of REAL

abs (x2 - z) is V11() real ext-real Element of REAL

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of the carrier of M

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

x1 is Element of the carrier of M

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) - (((M,x1) .: P)) is V11() real ext-real Element of REAL

abs ((((M,Q) .: P)) - (((M,x1) .: P))) is V11() real ext-real Element of REAL

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

x2 is Element of the carrier of (TopSpaceMetr M)

(M,Q) . x2 is V11() real ext-real Element of the carrier of R^1

Family_open_set M is Element of K6(K6( the carrier of M))

K6( the carrier of M) is non empty set

K6(K6( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

y is Element of the carrier of (TopSpaceMetr M)

(M,x1) . y is V11() real ext-real Element of the carrier of R^1

c

dist (c

(M,x1) . c

z is Element of the carrier of M

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

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

(dist (z,Q)) + (dist (Q,x1)) is V11() real ext-real Element of REAL

(dist (c

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

- ((dist (c

(M,Q) . z is set

dist (c

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

(dist (c

(dist (c

(dist (z,Q)) - (dist (c

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

the carrier of M is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

Q is Element of the carrier of M

(M,P) . Q is set

x1 is Element of the carrier of M

(M,P) . x1 is set

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

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

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

x2 - z is V11() real ext-real Element of REAL

abs (x2 - z) is V11() real ext-real Element of REAL

(M,Q) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,Q) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,Q) .: P)) is V11() real ext-real Element of REAL

(((M,Q) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,Q) .: P)) is V11() real ext-real Element of REAL

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

[#] R^1 is non empty non proper V47() V48() V49() Element of K6( the carrier of R^1)

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

Q is V47() V48() V49() Element of K6( the carrier of R^1)

(M,P) " Q is Element of K6( the carrier of (TopSpaceMetr M))

the carrier of M is non empty set

x1 is Element of the carrier of M

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

x2 is V11() real ext-real Element of the carrier of RealSpace

(M,P) . x1 is set

the carrier of (TopSpaceMetr RealSpace) is non empty set

K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set

z is Element of K6( the carrier of (TopSpaceMetr RealSpace))

y is V11() real ext-real set

Ball (x2,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is non empty set

c

Ball (x1,c

K6( the carrier of M) is non empty set

(M,P) " z is Element of K6( the carrier of (TopSpaceMetr M))

z is set

z is Element of the carrier of M

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

q is V11() real ext-real Element of the carrier of RealSpace

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

c

(((M,x1) .: P)) - (((M,z) .: P)) is V11() real ext-real Element of REAL

abs ((((M,x1) .: P)) - (((M,z) .: P))) is V11() real ext-real Element of REAL

(abs ((((M,x1) .: P)) - (((M,z) .: P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL

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

Ball (x2,c

dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) . z is set

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,P) .: Q)) is V11() real ext-real Element of REAL

(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)

upper_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

Q is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

(M,P) .: Q is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,P) .: Q)) is V11() real ext-real Element of REAL

(((M,P) .: Q)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,P) .: Q)) is V11() real ext-real Element of REAL

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set

K6( the carrier of (TopSpaceMetr M)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

K7( the carrier of (TopSpaceMetr M), the carrier of R^1) is non empty set

K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1)) is non empty set

Q is V47() V48() V49() Element of K6( the carrier of R^1)

(M,P) " Q is Element of K6( the carrier of (TopSpaceMetr M))

the carrier of M is non empty set

x1 is Element of the carrier of M

(M,P) . x1 is set

the carrier of (TopSpaceMetr RealSpace) is non empty set

K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set

(M,x1) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,x1) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,x1) .: P)) is V11() real ext-real Element of REAL

(((M,x1) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,x1) .: P)) is V11() real ext-real Element of REAL

z is V11() real ext-real Element of the carrier of RealSpace

x2 is Element of K6( the carrier of (TopSpaceMetr RealSpace))

y is V11() real ext-real set

Ball (z,y) is V47() V48() V49() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is non empty set

c

Ball (x1,c

K6( the carrier of M) is non empty set

(M,P) " x2 is Element of K6( the carrier of (TopSpaceMetr M))

z is set

z is Element of the carrier of M

(M,z) is Relation-like the carrier of (TopSpaceMetr M) -defined the carrier of R^1 -valued Function-like V30( the carrier of (TopSpaceMetr M), the carrier of R^1) Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of R^1))

(M,z) .: P is V47() V48() V49() Element of K6( the carrier of R^1)

(((M,z) .: P)) is V11() real ext-real Element of REAL

(((M,z) .: P)) is V47() V48() V49() Element of K6(REAL)

lower_bound (((M,z) .: P)) is V11() real ext-real Element of REAL

q is V11() real ext-real Element of the carrier of RealSpace

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

c

(((M,x1) .: P)) - (((M,z) .: P)) is V11() real ext-real Element of REAL

abs ((((M,x1) .: P)) - (((M,z) .: P))) is V11() real ext-real Element of REAL

(abs ((((M,x1) .: P)) - (((M,z) .: P)))) + (dist (x1,z)) is V11() real ext-real Element of REAL

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

Ball (z,c

dom (M,P) is Element of K6( the carrier of (TopSpaceMetr M))

(M,P) . z is set

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

Ball (x1,x2) is Element of K6( the carrier of M)

K6( the carrier of M) is non empty set

M is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr M) is non empty set