:: METRIC_6 semantic presentation

REAL is non empty V45() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is set

COMPLEX is non empty V45() set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative Element of NAT

[:1,1:] is set

bool [:1,1:] is set

[:[:1,1:],1:] is set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative Element of NAT

[:2,2:] is set

[:[:2,2:],REAL:] is set

bool [:[:2,2:],REAL:] is set

RAT is non empty V45() set

INT is non empty V45() set

bool NAT is set

bool [:REAL,REAL:] is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative Element of NAT

[:NAT,REAL:] is set

bool [:NAT,REAL:] is set

[:NAT,NAT:] is set

bool [:NAT,NAT:] is set

X is Reflexive discerning symmetric triangle MetrStruct

the carrier of X is set

V is Element of the carrier of X

y is Element of the carrier of X

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

r is Element of the carrier of X

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

(dist (V,y)) - (dist (r,y)) is V24() real ext-real Element of REAL

abs ((dist (V,y)) - (dist (r,y))) is V24() real ext-real Element of REAL

dist (V,r) is V24() real ext-real Element of REAL

dist (r,V) is V24() real ext-real Element of REAL

(dist (r,V)) + (dist (V,y)) is V24() real ext-real Element of REAL

(dist (r,y)) - (dist (V,y)) is V24() real ext-real Element of REAL

- (dist (V,r)) is V24() real ext-real Element of REAL

- ((dist (r,y)) - (dist (V,y))) is V24() real ext-real Element of REAL

(dist (V,r)) + (dist (r,y)) is V24() real ext-real Element of REAL

X is non empty set

[:X,X:] is set

[:[:X,X:],REAL:] is set

bool [:[:X,X:],REAL:] is set

V is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

y is Element of X

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

1 / 2 is V24() real ext-real non negative Element of REAL

V . (y,y) is V24() real ext-real Element of REAL

(1 / 2) * (V . (y,y)) is V24() real ext-real Element of REAL

(1 / 2) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative Element of REAL

1 * (V . (y,r)) is V24() real ext-real Element of REAL

(1 * (V . (y,r))) + (V . (y,r)) is V24() real ext-real Element of REAL

(1 / 2) * ((1 * (V . (y,r))) + (V . (y,r))) is V24() real ext-real Element of REAL

V . (r,y) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (r,y)) is V24() real ext-real Element of REAL

(1 / 2) * ((V . (y,r)) + (V . (r,y))) is V24() real ext-real Element of REAL

X is non empty set

[:X,X:] is set

[:[:X,X:],REAL:] is set

bool [:[:X,X:],REAL:] is set

V is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

y is Element of X

V . (y,y) is V24() real ext-real Element of REAL

y is Element of X

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

x is Element of X

s is Element of X

V . (x,s) is V24() real ext-real Element of REAL

y is Element of X

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (r,y) is V24() real ext-real Element of REAL

y is Element of X

x is Element of X

V . (y,x) is V24() real ext-real Element of REAL

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (r,x) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL

y is Element of X

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

x is Element of X

s is Element of X

V . (x,s) is V24() real ext-real Element of REAL

e is Element of X

e is Element of X

V . (e,e) is V24() real ext-real Element of REAL

V . (e,e) is V24() real ext-real Element of REAL

k is Element of X

n is Element of X

V . (k,n) is V24() real ext-real Element of REAL

k is Element of X

V . (k,k) is V24() real ext-real Element of REAL

V . (k,n) is V24() real ext-real Element of REAL

(V . (k,k)) + (V . (k,n)) is V24() real ext-real Element of REAL

X is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

the distance of X is Relation-like [: the carrier of X, the carrier of X:] -defined REAL -valued Function-like V29([: the carrier of X, the carrier of X:]) V30([: the carrier of X, the carrier of X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:],REAL:] is set

bool [:[: the carrier of X, the carrier of X:],REAL:] is set

X is non empty set

[:X,X:] is set

[:[:X,X:],REAL:] is set

bool [:[:X,X:],REAL:] is set

V is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

y is Element of X

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (r,y) is V24() real ext-real Element of REAL

V . (y,y) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (y,y)) is V24() real ext-real Element of REAL

(V . (y,r)) + 0 is V24() real ext-real Element of REAL

V . (r,r) is V24() real ext-real Element of REAL

(V . (r,y)) + (V . (r,r)) is V24() real ext-real Element of REAL

(V . (r,y)) + 0 is V24() real ext-real Element of REAL

y is Element of X

x is Element of X

V . (y,x) is V24() real ext-real Element of REAL

r is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (r,x) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL

V . (r,y) is V24() real ext-real Element of REAL

(V . (r,y)) + (V . (r,x)) is V24() real ext-real Element of REAL

r is Element of X

x is Element of X

V . (r,x) is V24() real ext-real Element of REAL

y is Element of X

V . (r,y) is V24() real ext-real Element of REAL

V . (y,x) is V24() real ext-real Element of REAL

(V . (r,y)) + (V . (y,x)) is V24() real ext-real Element of REAL

V . (y,r) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL

r is Element of X

x is Element of X

V . (r,x) is V24() real ext-real Element of REAL

y is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (y,x) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL

r is Element of X

x is Element of X

V . (r,x) is V24() real ext-real Element of REAL

y is Element of X

V . (y,r) is V24() real ext-real Element of REAL

V . (y,x) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL

e is Element of X

e is Element of X

V . (e,e) is V24() real ext-real Element of REAL

s is Element of X

V . (s,e) is V24() real ext-real Element of REAL

V . (s,e) is V24() real ext-real Element of REAL

(V . (s,e)) + (V . (s,e)) is V24() real ext-real Element of REAL

X is non empty set

[:X,X:] is set

[:[:X,X:],REAL:] is set

bool [:[:X,X:],REAL:] is set

V is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

y is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

r is Element of X

x is Element of X

y . (r,x) is V24() real ext-real Element of REAL

V . (r,x) is V24() real ext-real Element of REAL

1 + (V . (r,x)) is V24() real ext-real Element of REAL

(V . (r,x)) / (1 + (V . (r,x))) is V24() real ext-real Element of REAL

y is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

r is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

x is Element of X

s is Element of X

y . (x,s) is V24() real ext-real Element of REAL

r . (x,s) is V24() real ext-real Element of REAL

V . (x,s) is V24() real ext-real Element of REAL

1 + (V . (x,s)) is V24() real ext-real Element of REAL

(V . (x,s)) / (1 + (V . (x,s))) is V24() real ext-real Element of REAL

X is non empty set

[:X,X:] is set

[:[:X,X:],REAL:] is set

bool [:[:X,X:],REAL:] is set

V is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

(X,V) is Relation-like [:X,X:] -defined REAL -valued Function-like V29([:X,X:]) V30([:X,X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:X,X:],REAL:]

y is Element of X

x is Element of X

(X,V) . (y,x) is V24() real ext-real Element of REAL

r is Element of X

(X,V) . (y,r) is V24() real ext-real Element of REAL

(X,V) . (r,x) is V24() real ext-real Element of REAL

((X,V) . (y,r)) + ((X,V) . (r,x)) is V24() real ext-real Element of REAL

V . (y,r) is V24() real ext-real Element of REAL

V . (y,x) is V24() real ext-real Element of REAL

V . (r,x) is V24() real ext-real Element of REAL

1 + (V . (y,r)) is V24() real ext-real Element of REAL

(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL

1 + (V . (y,x)) is V24() real ext-real Element of REAL

(V . (y,x)) / (1 + (V . (y,x))) is V24() real ext-real Element of REAL

1 + (V . (r,x)) is V24() real ext-real Element of REAL

(V . (r,x)) / (1 + (V . (r,x))) is V24() real ext-real Element of REAL

(1 + (V . (y,r))) * (1 + (V . (r,x))) is V24() real ext-real Element of REAL

((V . (y,r)) / (1 + (V . (y,r)))) + ((V . (r,x)) / (1 + (V . (r,x)))) is V24() real ext-real Element of REAL

(V . (y,r)) * (1 + (V . (r,x))) is V24() real ext-real Element of REAL

(V . (r,x)) * (1 + (V . (y,r))) is V24() real ext-real Element of REAL

((V . (y,r)) * (1 + (V . (r,x)))) + ((V . (r,x)) * (1 + (V . (y,r)))) is V24() real ext-real Element of REAL

(((V . (y,r)) * (1 + (V . (r,x)))) + ((V . (r,x)) * (1 + (V . (y,r))))) / ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL

(V . (y,r)) * 1 is V24() real ext-real Element of REAL

(V . (y,r)) * (V . (r,x)) is V24() real ext-real Element of REAL

((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x))) is V24() real ext-real Element of REAL

(V . (r,x)) * 1 is V24() real ext-real Element of REAL

(V . (r,x)) * (V . (y,r)) is V24() real ext-real Element of REAL

((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r))) is V24() real ext-real Element of REAL

(((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x)))) + (((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r)))) is V24() real ext-real Element of REAL

((((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x)))) + (((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r))))) / ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL

(((V . (y,r)) / (1 + (V . (y,r)))) + ((V . (r,x)) / (1 + (V . (r,x))))) - ((V . (y,x)) / (1 + (V . (y,x)))) is V24() real ext-real Element of REAL

(V . (y,r)) + ((V . (y,r)) * (V . (r,x))) is V24() real ext-real Element of REAL

(V . (r,x)) + ((V . (r,x)) * (V . (y,r))) is V24() real ext-real Element of REAL

((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r)))) is V24() real ext-real Element of REAL

(((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x))) is V24() real ext-real Element of REAL

(V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL

((((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x)))) - ((V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x))))) is V24() real ext-real Element of REAL

((1 + (V . (y,r))) * (1 + (V . (r,x)))) * (1 + (V . (y,x))) is V24() real ext-real Element of REAL

(((((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x)))) - ((V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x)))))) / (((1 + (V . (y,r))) * (1 + (V . (r,x)))) * (1 + (V . (y,x)))) is V24() real ext-real Element of REAL

(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL

((V . (y,r)) + (V . (r,x))) - (V . (y,x)) is V24() real ext-real Element of REAL

(V . (r,x)) + (V . (y,r)) is V24() real ext-real Element of REAL

((V . (r,x)) + (V . (y,r))) - (V . (y,x)) is V24() real ext-real Element of REAL

((V . (r,x)) * (V . (y,r))) * (V . (y,x)) is V24() real ext-real Element of REAL

((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x))) is V24() real ext-real Element of REAL

((V . (y,r)) * (V . (r,x))) + (((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x)))) is V24() real ext-real Element of REAL

(((V . (r,x)) + (V . (y,r))) - (V . (y,x))) + (((V . (y,r)) * (V . (r,x))) + (((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x))))) is V24() real ext-real Element of REAL

y is Element of X

r is Element of X

(X,V) . (y,r) is V24() real ext-real Element of REAL

V . (y,r) is V24() real ext-real Element of REAL

1 + (V . (y,r)) is V24() real ext-real Element of REAL

(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL

V . (y,r) is V24() real ext-real Element of REAL

1 + (V . (y,r)) is V24() real ext-real Element of REAL

(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL

y is Element of X

r is Element of X

(X,V) . (y,r) is V24() real ext-real Element of REAL

(X,V) . (r,y) is V24() real ext-real Element of REAL

V . (y,r) is V24() real ext-real Element of REAL

1 + (V . (y,r)) is V24() real ext-real Element of REAL

(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL

V . (r,y) is V24() real ext-real Element of REAL

(V . (r,y)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL

1 + (V . (r,y)) is V24() real ext-real Element of REAL

(V . (r,y)) / (1 + (V . (r,y))) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

{V} is non empty Element of bool the carrier of X

bool the carrier of X is set

y is Relation-like Function-like set

dom y is set

rng y is set

r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

rng r is set

X is non empty MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

X is non empty symmetric triangle MetrStruct

the carrier of X is non empty set

bool the carrier of X is set

V is Element of bool the carrier of X

y is Element of the carrier of X

r is V24() real ext-real Element of REAL

2 * r is V24() real ext-real Element of REAL

x is V24() real ext-real Element of REAL

s is Element of the carrier of X

Ball (s,x) is Element of bool the carrier of X

e is set

1 * r is V24() real ext-real Element of REAL

e is Element of the carrier of X

dist (s,e) is V24() real ext-real Element of REAL

the Element of the carrier of X is Element of the carrier of X

1 / 2 is V24() real ext-real non negative Element of REAL

r is V24() real ext-real non negative Element of REAL

x is Element of the carrier of X

Ball (x,r) is Element of bool the carrier of X

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

r is Element of the carrier of X

Ball (r,y) is Element of bool the carrier of X

2 * y is V24() real ext-real Element of REAL

x is Element of the carrier of X

s is Element of the carrier of X

dist (x,s) is V24() real ext-real Element of REAL

dist (r,s) is V24() real ext-real Element of REAL

dist (r,x) is V24() real ext-real Element of REAL

dist (x,r) is V24() real ext-real Element of REAL

(dist (x,r)) + (dist (r,s)) is V24() real ext-real Element of REAL

y + y is V24() real ext-real Element of REAL

dist (x,s) is V24() real ext-real Element of REAL

X is non empty MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

bool the carrier of X is set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

rng V is set

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

r is Element of the carrier of X

Ball (r,y) is bounded Element of bool the carrier of X

bool the carrier of X is set

x is V24() real ext-real Element of REAL

s is Element of the carrier of X

Ball (s,x) is bounded Element of bool the carrier of X

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . e is Element of the carrier of X

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . e is Element of the carrier of X

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

r is Element of the carrier of X

Ball (r,y) is bounded Element of bool the carrier of X

bool the carrier of X is set

rng V is set

x is set

dom V is set

s is set

V . s is set

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is Element of the carrier of X

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is Element of the carrier of X

r is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . x is V24() real ext-real Element of REAL

V . x is Element of the carrier of X

dist ((V . x),y) is V24() real ext-real Element of REAL

r is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . s is V24() real ext-real Element of REAL

V . s is Element of the carrier of X

dist ((V . s),y) is V24() real ext-real Element of REAL

x . s is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . x is V24() real ext-real Element of REAL

V . x is Element of the carrier of X

y . x is Element of the carrier of X

dist ((V . x),(y . x)) is V24() real ext-real Element of REAL

r is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . s is V24() real ext-real Element of REAL

V . s is Element of the carrier of X

y . s is Element of the carrier of X

dist ((V . s),(y . s)) is V24() real ext-real Element of REAL

x . s is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim y is Element of the carrier of X

r is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim y is Element of the carrier of X

r is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim V is Element of the carrier of X

y is Element of the carrier of X

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

(X,y,V) is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (X,y,V) is V24() real ext-real Element of REAL

r is V24() real ext-real set

x is V24() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

(X,y,V) . e is V24() real ext-real Element of REAL

((X,y,V) . e) - 0 is V24() real ext-real Element of REAL

abs (((X,y,V) . e) - 0) is V24() real ext-real Element of REAL

y . e is Element of the carrier of X

dist ((y . e),V) is V24() real ext-real Element of REAL

r is V24() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

dist ((y . e),V) is V24() real ext-real Element of REAL

(X,y,V) . e is V24() real ext-real Element of REAL

((X,y,V) . e) - 0 is V24() real ext-real Element of REAL

abs (((X,y,V) . e) - 0) is V24() real ext-real Element of REAL

abs (dist ((y . e),V)) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

bool the carrier of X is set

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

dist (V,(y . e)) is V24() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

bool the carrier of X is set

Family_open_set X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

r is Element of bool the carrier of X

x is V24() real ext-real Element of REAL

Ball (V,x) is bounded Element of bool the carrier of X

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

bool the carrier of X is set

Family_open_set X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

dist (V,V) is V24() real ext-real Element of REAL

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

dist ((y . e),V) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

bool the carrier of X is set

bool the carrier of X is set

Family_open_set X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is set

r is Element of bool the carrier of X

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

bool the carrier of X is set

Family_open_set X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is V24() real ext-real Element of REAL

Ball (V,r) is bounded Element of bool the carrier of X

r is Element of bool the carrier of X

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

bool the carrier of X is set

x is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of x is non empty set

[:NAT, the carrier of x:] is set

bool [:NAT, the carrier of x:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is Element of bool the carrier of X

Family_open_set X is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is set

bool the carrier of x is set

s is Element of the carrier of x

Family_open_set x is Element of bool (bool the carrier of x)

bool (bool the carrier of x) is set

e is non empty Relation-like NAT -defined the carrier of x -valued Function-like V29( NAT ) V30( NAT , the carrier of x) Element of bool [:NAT, the carrier of x:]

e is V24() real ext-real Element of REAL

Ball (s,e) is bounded Element of bool the carrier of x

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim y is Element of the carrier of X

dist ((lim V),(lim y)) is V24() real ext-real Element of REAL

(X,V,y) is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (X,V,y) is V24() real ext-real Element of REAL

r is Element of the carrier of X

x is Element of the carrier of X

dist (r,x) is V24() real ext-real Element of REAL

s is V24() real ext-real set

e is V24() real ext-real Element of REAL

e / 2 is V24() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e + k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

(X,V,y) . n is V24() real ext-real Element of REAL

((X,V,y) . n) - (dist (r,x)) is V24() real ext-real Element of REAL

abs (((X,V,y) . n) - (dist (r,x))) is V24() real ext-real Element of REAL

V . n is Element of the carrier of X

y . n is Element of the carrier of X

dist ((V . n),(y . n)) is V24() real ext-real Element of REAL

dist (r,(y . n)) is V24() real ext-real Element of REAL

(dist ((V . n),(y . n))) - (dist (r,(y . n))) is V24() real ext-real Element of REAL

abs ((dist ((V . n),(y . n))) - (dist (r,(y . n)))) is V24() real ext-real Element of REAL

dist ((V . n),r) is V24() real ext-real Element of REAL

dist ((y . n),r) is V24() real ext-real Element of REAL

dist (x,r) is V24() real ext-real Element of REAL

(dist ((y . n),r)) - (dist (x,r)) is V24() real ext-real Element of REAL

abs ((dist ((y . n),r)) - (dist (x,r))) is V24() real ext-real Element of REAL

dist ((y . n),x) is V24() real ext-real Element of REAL

(dist ((V . n),(y . n))) - (dist ((y . n),r)) is V24() real ext-real Element of REAL

abs ((dist ((V . n),(y . n))) - (dist ((y . n),r))) is V24() real ext-real Element of REAL

(dist ((y . n),r)) - (dist (r,x)) is V24() real ext-real Element of REAL

abs ((dist ((y . n),r)) - (dist (r,x))) is V24() real ext-real Element of REAL

(abs ((dist ((V . n),(y . n))) - (dist ((y . n),r)))) + (abs ((dist ((y . n),r)) - (dist (r,x)))) is V24() real ext-real Element of REAL

(dist ((V . n),r)) + (dist ((y . n),x)) is V24() real ext-real Element of REAL

((X,V,y) . n) - (dist ((lim V),(lim y))) is V24() real ext-real Element of REAL

abs (((X,V,y) . n) - (dist ((lim V),(lim y)))) is V24() real ext-real Element of REAL

(dist ((V . n),(y . n))) - (dist (r,x)) is V24() real ext-real Element of REAL

abs ((dist ((V . n),(y . n))) - (dist (r,x))) is V24() real ext-real Element of REAL

((dist ((V . n),(y . n))) - (dist ((y . n),r))) + ((dist ((y . n),r)) - (dist (r,x))) is V24() real ext-real Element of REAL

abs (((dist ((V . n),(y . n))) - (dist ((y . n),r))) + ((dist ((y . n),r)) - (dist (r,x)))) is V24() real ext-real Element of REAL

(e / 2) + (e / 2) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is Element of the carrier of X

r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim r is Element of the carrier of X

(X,r,r) is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real set

(X,r,r) . x is V24() real ext-real Element of REAL

r . x is Element of the carrier of X

dist ((r . x),(r . x)) is V24() real ext-real Element of REAL

(X,r,r) . 0 is V24() real ext-real Element of REAL

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

lim (X,r,r) is V24() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

(X,r,r) . x is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is Element of the carrier of X

r is V24() real ext-real Element of REAL

x is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . s is Element of the carrier of X

dist ((V . s),y) is V24() real ext-real Element of REAL

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

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . s is Element of the carrier of X

dist ((V . s),y) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is Element of the carrier of X

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

x is non empty Relation-like NAT -defined NAT -valued Function-like V29( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

y * x is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of y

s is V24() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . k is Element of the carrier of X

dist ((r . k),V) is V24() real ext-real Element of REAL

dom y is set

dom x is set

x . k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

dom (y * x) is set

y . (x . k) is Element of the carrier of X

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

r . k is Element of the carrier of X

dist ((r . k),V) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r is non empty Relation-like NAT -defined NAT -valued Function-like V29( NAT ) V30( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

V * r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of V

x is V24() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . k is Element of the carrier of X

dist ((y . e),(y . k)) is V24() real ext-real Element of REAL

r . k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

dom V is set

dom r is set

dom (V * r) is set

V . (r . k) is Element of the carrier of X

r . e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . (r . e) is Element of the carrier of X

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

y . e is Element of the carrier of X

y . k is Element of the carrier of X

dist ((y . e),(y . k)) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim V is Element of the carrier of X

y is Element of the carrier of X

(X,V,y) is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r is V24() real ext-real set

x is V24() real ext-real Element of REAL

Ball (y,x) is bounded Element of bool the carrier of X

bool the carrier of X is set

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . s is Element of the carrier of X

(X,V,y) . s is V24() real ext-real Element of REAL

dist ((V . s),y) is V24() real ext-real Element of REAL

abs ((X,V,y) . s) is V24() real ext-real Element of REAL

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . s is Element of the carrier of X

V . e is Element of the carrier of X

dist ((V . s),(V . e)) is V24() real ext-real Element of REAL

y is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

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

r is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . r is Element of the carrier of X

(X,V,(V . r)) is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is V24() real ext-real set

s is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . s is Element of the carrier of X

dist ((V . s),(V . r)) is V24() real ext-real Element of REAL

(X,V,(V . r)) . s is V24() real ext-real Element of REAL

abs ((X,V,(V . r)) . s) is V24() real ext-real Element of REAL

x + y is V24() real ext-real Element of REAL

s is V24() real ext-real Element of REAL

e is Element of the carrier of X

Ball (e,s) is bounded Element of bool the carrier of X

bool the carrier of X is set

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . e is Element of the carrier of X

dist ((V . e),(V . r)) is V24() real ext-real Element of REAL

dist ((V . e),e) is V24() real ext-real Element of REAL

dist ((V . e),(V . r)) is V24() real ext-real Element of REAL

dist ((V . e),e) is V24() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real Element of NAT

V . e is Element of the carrier of X

s is V24() real ext-real Element of REAL

e is Element of the carrier of X

Ball (e,s) is bounded Element of bool the carrier of X

bool the carrier of X is set

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

the Element of the carrier of X is Element of the carrier of X

{ the Element of the carrier of X} is non empty Element of bool the carrier of X

bool the carrier of X is set

y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

rng y is set

X is non empty Reflexive symmetric triangle MetrStruct

the carrier of X is non empty set

bool the carrier of X is set

V is bounded Element of bool the carrier of X

y is Element of the carrier of X

r is V24() real ext-real Element of REAL

x is Element of the carrier of X

Ball (x,r) is bounded Element of bool the carrier of X

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

r + (dist (x,y)) is V24() real ext-real Element of REAL

s is V24() real ext-real Element of REAL

Ball (y,s) is bounded Element of bool the carrier of X

r + 0 is V24() real ext-real Element of REAL

e is set

e is Element of the carrier of X

dist (e,x) is V24() real ext-real Element of REAL

(dist (e,x)) + (dist (x,y)) is V24() real ext-real Element of REAL

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