:: TBSP_1 semantic presentation

REAL is non empty non trivial non finite V112() V113() V114() V118() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() Element of K10(REAL)

K10(REAL) is non empty set

COMPLEX is non empty non trivial non finite V112() V118() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() set

K10(NAT) is non empty set

K10(NAT) is non empty set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

K11(1,1) is non empty set

K10(K11(1,1)) is non empty set

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

K10(K11(K11(1,1),1)) is non empty set

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

K10(K11(K11(1,1),REAL)) is non empty set

K11(REAL,REAL) is non empty set

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

K10(K11(K11(REAL,REAL),REAL)) is non empty set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

K11(2,2) is non empty set

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

K10(K11(K11(2,2),REAL)) is non empty set

RAT is non empty non trivial non finite V112() V113() V114() V115() V118() set

INT is non empty non trivial non finite V112() V113() V114() V115() V116() V118() set

{} is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() set

the empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() set is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() set

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

0 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V110() V111() V112() V113() V114() V115() V116() V117() V118() Element of NAT

K11(NAT,REAL) is non empty set

K10(K11(NAT,REAL)) is non empty set

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

4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T is ext-real V30() real Element of REAL

S1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T to_power S1 is ext-real V30() real Element of REAL

A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T to_power A is ext-real V30() real Element of REAL

T is ext-real V30() real Element of REAL

S1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T to_power S1 is ext-real V30() real Element of REAL

S1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T to_power (S1 + 1) is ext-real V30() real Element of REAL

T to_power 1 is ext-real V30() real Element of REAL

(T to_power S1) * (T to_power 1) is ext-real V30() real Element of REAL

(T to_power S1) * T is ext-real V30() real Element of REAL

T to_power 0 is ext-real V30() real Element of REAL

T is ext-real V30() real Element of REAL

S1 is ext-real V30() real Element of REAL

A is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) Element of K10(K11(NAT,REAL))

lim A is ext-real V30() real Element of REAL

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T to_power (p + 1) is ext-real V30() real Element of REAL

A . p is ext-real V30() real Element of REAL

(A . p) - 0 is ext-real V30() real Element of REAL

abs ((A . p) - 0) is ext-real V30() real Element of REAL

abs (T to_power (p + 1)) is ext-real V30() real Element of REAL

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like Function-like set

dom S1 is set

A is set

S1 . A is set

rng S1 is set

A is set

rng S1 is set

p is set

S1 . p is set

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like Function-like set

dom S1 is set

A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . A is set

A is set

S1 . A is set

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

T is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

A is Element of the carrier of T

p is Element of the carrier of T

dist (A,p) is ext-real V30() real Element of REAL

(dist (A,p)) / 4 is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . (C + B) is Element of the carrier of T

dist ((S1 . (C + B)),p) is ext-real V30() real Element of REAL

dist (A,(S1 . (C + B))) is ext-real V30() real Element of REAL

(dist (A,(S1 . (C + B)))) + (dist ((S1 . (C + B)),p)) is ext-real V30() real Element of REAL

dist ((S1 . (C + B)),A) is ext-real V30() real Element of REAL

((dist (A,p)) / 4) + ((dist (A,p)) / 4) is ext-real V30() real Element of REAL

(dist (A,p)) / 2 is ext-real V30() real Element of REAL

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . A is set

S1 . A is Element of the carrier of T

T is non empty MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

A is non empty symmetric MetrStruct

the carrier of A is non empty set

K11(NAT, the carrier of A) is non empty set

K10(K11(NAT, the carrier of A)) is non empty set

p is Relation-like NAT -defined the carrier of A -valued Function-like V33( NAT , the carrier of A) Element of K10(K11(NAT, the carrier of A))

B is Element of the carrier of A

C is ext-real V30() real Element of REAL

C / 2 is ext-real V30() real Element of REAL

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . C is Element of the carrier of T

S1 . x is Element of the carrier of T

dist ((S1 . C),(S1 . x)) is ext-real V30() real Element of REAL

(A,p,x) is Element of the carrier of A

dist ((A,p,x),B) is ext-real V30() real Element of REAL

(A,p,C) is Element of the carrier of A

dist ((A,p,C),B) is ext-real V30() real Element of REAL

(C / 2) + (C / 2) is ext-real V30() real Element of REAL

dist (B,(A,p,x)) is ext-real V30() real Element of REAL

(dist ((A,p,C),B)) + (dist (B,(A,p,x))) is ext-real V30() real Element of REAL

dist ((A,p,C),(A,p,x)) is ext-real V30() real Element of REAL

T is non empty symmetric triangle MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

T is non empty symmetric MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

A is ext-real V30() real Element of REAL

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B + C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,(B + C)) is Element of the carrier of T

(T,S1,B) is Element of the carrier of T

dist ((T,S1,(B + C)),(T,S1,B)) is ext-real V30() real Element of REAL

A is ext-real V30() real Element of REAL

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . B is Element of the carrier of T

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

S1 . C is Element of the carrier of T

dist ((S1 . B),(S1 . C)) is ext-real V30() real Element of REAL

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real set

B + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B + z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,C) is Element of the carrier of T

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,x) is Element of the carrier of T

dist ((T,S1,C),(T,S1,x)) is ext-real V30() real Element of REAL

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real set

C + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

T is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of T is non empty set

K11( the carrier of T, the carrier of T) is non empty set

K10(K11( the carrier of T, the carrier of T)) is non empty set

S1 is Relation-like the carrier of T -defined the carrier of T -valued Function-like V33( the carrier of T, the carrier of T) contraction Element of K10(K11( the carrier of T, the carrier of T))

A is ext-real V30() real Element of REAL

1 - A is ext-real V30() real Element of REAL

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

the Element of the carrier of T is Element of the carrier of T

B is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

(T,B,0) is Element of the carrier of T

B is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

(T,B,0) is Element of the carrier of T

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,B,(C + 1)) is Element of the carrier of T

(T,B,C) is Element of the carrier of T

S1 . (T,B,C) is Element of the carrier of T

p is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

p is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

(T,p,1) is Element of the carrier of T

(T,p,0) is Element of the carrier of T

dist ((T,p,1),(T,p,0)) is ext-real V30() real Element of REAL

S1 . (T,p,0) is Element of the carrier of T

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(0 + 1)) is Element of the carrier of T

C is Element of the carrier of T

S1 . C is Element of the carrier of T

dist (C,(T,p,0)) is ext-real V30() real Element of REAL

A * (dist (C,(T,p,0))) is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + 1)) is Element of the carrier of T

(T,p,C) is Element of the carrier of T

dist ((T,p,(C + 1)),(T,p,C)) is ext-real V30() real Element of REAL

A to_power C is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (A to_power C) is ext-real V30() real Element of REAL

(C + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,((C + 1) + 1)) is Element of the carrier of T

dist ((T,p,((C + 1) + 1)),(T,p,(C + 1))) is ext-real V30() real Element of REAL

A to_power (C + 1) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (A to_power (C + 1)) is ext-real V30() real Element of REAL

A * (dist ((T,p,(C + 1)),(T,p,C))) is ext-real V30() real Element of REAL

A * ((dist ((T,p,1),(T,p,0))) * (A to_power C)) is ext-real V30() real Element of REAL

S1 . (T,p,(C + 1)) is Element of the carrier of T

dist ((S1 . (T,p,(C + 1))),(T,p,(C + 1))) is ext-real V30() real Element of REAL

S1 . (T,p,C) is Element of the carrier of T

dist ((S1 . (T,p,(C + 1))),(S1 . (T,p,C))) is ext-real V30() real Element of REAL

A * (A to_power C) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (A * (A to_power C)) is ext-real V30() real Element of REAL

A to_power 1 is ext-real V30() real Element of REAL

(A to_power C) * (A to_power 1) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((A to_power C) * (A to_power 1)) is ext-real V30() real Element of REAL

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(0 + 1)) is Element of the carrier of T

dist ((T,p,(0 + 1)),(T,p,0)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * 1 is ext-real V30() real Element of REAL

A to_power 0 is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (A to_power 0) is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,C) is Element of the carrier of T

dist ((T,p,C),(T,p,0)) is ext-real V30() real Element of REAL

A to_power C is ext-real V30() real Element of REAL

1 - (A to_power C) is ext-real V30() real Element of REAL

(1 - (A to_power C)) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - (A to_power C)) / (1 - A)) is ext-real V30() real Element of REAL

C + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + 1)) is Element of the carrier of T

dist ((T,p,(C + 1)),(T,p,0)) is ext-real V30() real Element of REAL

A to_power (C + 1) is ext-real V30() real Element of REAL

1 - (A to_power (C + 1)) is ext-real V30() real Element of REAL

(1 - (A to_power (C + 1))) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - (A to_power (C + 1))) / (1 - A)) is ext-real V30() real Element of REAL

dist ((T,p,(C + 1)),(T,p,C)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (A to_power C) is ext-real V30() real Element of REAL

(dist ((T,p,(C + 1)),(T,p,C))) + (dist ((T,p,C),(T,p,0))) is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) * (A to_power C)) + ((dist ((T,p,1),(T,p,0))) * ((1 - (A to_power C)) / (1 - A))) is ext-real V30() real Element of REAL

(A to_power C) + ((1 - (A to_power C)) / (1 - A)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((A to_power C) + ((1 - (A to_power C)) / (1 - A))) is ext-real V30() real Element of REAL

(A to_power C) / (1 - A) is ext-real V30() real Element of REAL

((A to_power C) / (1 - A)) * (1 - A) is ext-real V30() real Element of REAL

(((A to_power C) / (1 - A)) * (1 - A)) + ((1 - (A to_power C)) / (1 - A)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((((A to_power C) / (1 - A)) * (1 - A)) + ((1 - (A to_power C)) / (1 - A))) is ext-real V30() real Element of REAL

(1 - A) * (A to_power C) is ext-real V30() real Element of REAL

((1 - A) * (A to_power C)) / (1 - A) is ext-real V30() real Element of REAL

(((1 - A) * (A to_power C)) / (1 - A)) + ((1 - (A to_power C)) / (1 - A)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((((1 - A) * (A to_power C)) / (1 - A)) + ((1 - (A to_power C)) / (1 - A))) is ext-real V30() real Element of REAL

1 * (A to_power C) is ext-real V30() real Element of REAL

A * (A to_power C) is ext-real V30() real Element of REAL

(1 * (A to_power C)) - (A * (A to_power C)) is ext-real V30() real Element of REAL

((1 * (A to_power C)) - (A * (A to_power C))) + (1 - (A to_power C)) is ext-real V30() real Element of REAL

(((1 * (A to_power C)) - (A * (A to_power C))) + (1 - (A to_power C))) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((((1 * (A to_power C)) - (A * (A to_power C))) + (1 - (A to_power C))) / (1 - A)) is ext-real V30() real Element of REAL

1 - (A * (A to_power C)) is ext-real V30() real Element of REAL

(1 - (A * (A to_power C))) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - (A * (A to_power C))) / (1 - A)) is ext-real V30() real Element of REAL

A to_power 1 is ext-real V30() real Element of REAL

(A to_power C) * (A to_power 1) is ext-real V30() real Element of REAL

1 - ((A to_power C) * (A to_power 1)) is ext-real V30() real Element of REAL

(1 - ((A to_power C) * (A to_power 1))) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - ((A to_power C) * (A to_power 1))) / (1 - A)) is ext-real V30() real Element of REAL

A to_power 0 is ext-real V30() real Element of REAL

1 - (A to_power 0) is ext-real V30() real Element of REAL

(1 - (A to_power 0)) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - (A to_power 0)) / (1 - A)) is ext-real V30() real Element of REAL

1 - 1 is ext-real V30() real Element of REAL

(1 - 1) / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - 1) / (1 - A)) is ext-real V30() real Element of REAL

dist ((T,p,0),(T,p,0)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) / (1 - A) is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,C) is Element of the carrier of T

dist ((T,p,C),(T,p,0)) is ext-real V30() real Element of REAL

A to_power C is ext-real V30() real Element of REAL

1 - (A to_power C) is ext-real V30() real Element of REAL

(1 - (A to_power C)) / (1 - A) is ext-real V30() real Element of REAL

1 / (1 - A) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * ((1 - (A to_power C)) / (1 - A)) is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (1 / (1 - A)) is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,C) is Element of the carrier of T

A to_power C is ext-real V30() real Element of REAL

C + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + 1)) is Element of the carrier of T

A to_power (C + 1) is ext-real V30() real Element of REAL

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(C + 1) + B is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,((C + 1) + B)) is Element of the carrier of T

dist ((T,p,((C + 1) + B)),(T,p,(C + 1))) is ext-real V30() real Element of REAL

(T,p,B) is Element of the carrier of T

dist ((T,p,B),(T,p,0)) is ext-real V30() real Element of REAL

(A to_power (C + 1)) * (dist ((T,p,B),(T,p,0))) is ext-real V30() real Element of REAL

(A to_power C) * (dist ((T,p,B),(T,p,0))) is ext-real V30() real Element of REAL

A * ((A to_power C) * (dist ((T,p,B),(T,p,0)))) is ext-real V30() real Element of REAL

A * (A to_power C) is ext-real V30() real Element of REAL

(A * (A to_power C)) * (dist ((T,p,B),(T,p,0))) is ext-real V30() real Element of REAL

A to_power 1 is ext-real V30() real Element of REAL

(A to_power C) * (A to_power 1) is ext-real V30() real Element of REAL

((A to_power C) * (A to_power 1)) * (dist ((T,p,B),(T,p,0))) is ext-real V30() real Element of REAL

C + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(C + B) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,((C + B) + 1)) is Element of the carrier of T

dist ((T,p,((C + B) + 1)),(T,p,(C + 1))) is ext-real V30() real Element of REAL

(T,p,(C + B)) is Element of the carrier of T

S1 . (T,p,(C + B)) is Element of the carrier of T

dist ((S1 . (T,p,(C + B))),(T,p,(C + 1))) is ext-real V30() real Element of REAL

S1 . (T,p,C) is Element of the carrier of T

dist ((S1 . (T,p,(C + B))),(S1 . (T,p,C))) is ext-real V30() real Element of REAL

dist ((T,p,(C + B)),(T,p,C)) is ext-real V30() real Element of REAL

A * (dist ((T,p,(C + B)),(T,p,C))) is ext-real V30() real Element of REAL

A to_power 0 is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

0 + C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(0 + C)) is Element of the carrier of T

dist ((T,p,(0 + C)),(T,p,0)) is ext-real V30() real Element of REAL

(T,p,C) is Element of the carrier of T

dist ((T,p,C),(T,p,0)) is ext-real V30() real Element of REAL

(A to_power 0) * (dist ((T,p,C),(T,p,0))) is ext-real V30() real Element of REAL

1 * (dist ((T,p,C),(T,p,0))) is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + B)) is Element of the carrier of T

(T,p,C) is Element of the carrier of T

dist ((T,p,(C + B)),(T,p,C)) is ext-real V30() real Element of REAL

A to_power C is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) / (1 - A)) * (A to_power C) is ext-real V30() real Element of REAL

(T,p,B) is Element of the carrier of T

dist ((T,p,B),(T,p,0)) is ext-real V30() real Element of REAL

(A to_power C) * (dist ((T,p,B),(T,p,0))) is ext-real V30() real Element of REAL

(A to_power C) * ((dist ((T,p,1),(T,p,0))) / (1 - A)) is ext-real V30() real Element of REAL

(1 - A) / (dist ((T,p,1),(T,p,0))) is ext-real V30() real Element of REAL

C is ext-real V30() real Element of REAL

((1 - A) / (dist ((T,p,1),(T,p,0)))) * C is ext-real V30() real Element of REAL

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

A to_power B is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + x)) is Element of the carrier of T

(T,p,C) is Element of the carrier of T

dist ((T,p,(C + x)),(T,p,C)) is ext-real V30() real Element of REAL

A to_power C is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) / (1 - A)) * (((1 - A) / (dist ((T,p,1),(T,p,0)))) * C) is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) / (1 - A)) * (A to_power C) is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) / (1 - A)) * ((1 - A) / (dist ((T,p,1),(T,p,0)))) is ext-real V30() real Element of REAL

(((dist ((T,p,1),(T,p,0))) / (1 - A)) * ((1 - A) / (dist ((T,p,1),(T,p,0))))) * C is ext-real V30() real Element of REAL

(dist ((T,p,1),(T,p,0))) * (1 - A) is ext-real V30() real Element of REAL

((dist ((T,p,1),(T,p,0))) * (1 - A)) / ((dist ((T,p,1),(T,p,0))) * (1 - A)) is ext-real V30() real Element of REAL

(((dist ((T,p,1),(T,p,0))) * (1 - A)) / ((dist ((T,p,1),(T,p,0))) * (1 - A))) * C is ext-real V30() real Element of REAL

1 * C is ext-real V30() real Element of REAL

C is Element of the carrier of T

S1 . C is Element of the carrier of T

dist (C,(S1 . C)) is ext-real V30() real Element of REAL

(dist (C,(S1 . C))) / 4 is ext-real V30() real Element of REAL

C is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

C + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,p,(C + 1)) is Element of the carrier of T

dist ((T,p,(C + 1)),(S1 . C)) is ext-real V30() real Element of REAL

(T,p,C) is Element of the carrier of T

S1 . (T,p,C) is Element of the carrier of T

dist ((S1 . (T,p,C)),(S1 . C)) is ext-real V30() real Element of REAL

dist ((T,p,C),C) is ext-real V30() real Element of REAL

A * (dist ((T,p,C),C)) is ext-real V30() real Element of REAL

dist (C,(T,p,(C + 1))) is ext-real V30() real Element of REAL

(dist (C,(T,p,(C + 1)))) + (dist ((T,p,(C + 1)),(S1 . C))) is ext-real V30() real Element of REAL

(dist (C,(S1 . C))) / 2 is ext-real V30() real Element of REAL

((dist (C,(S1 . C))) / 4) + ((dist (C,(S1 . C))) / 4) is ext-real V30() real Element of REAL

B is Element of the carrier of T

S1 . B is Element of the carrier of T

dist (B,C) is ext-real V30() real Element of REAL

A * (dist (B,C)) is ext-real V30() real Element of REAL

C is Element of the carrier of T

S1 . C is Element of the carrier of T

T is non empty Reflexive symmetric triangle MetrStruct

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

the carrier of T is non empty set

Family_open_set T is Element of K10(K10( the carrier of T))

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

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

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

A is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

{ b

( p <= b

(T,A,p) is Element of the carrier of T

the carrier of (TopSpaceMetr T) is non empty set

K10( the carrier of (TopSpaceMetr T)) is non empty set

K10(K10( the carrier of (TopSpaceMetr T))) is non empty set

p is Element of K10(K10( the carrier of (TopSpaceMetr T)))

{ b

B is Element of K10(K10( the carrier of (TopSpaceMetr T)))

clf B is Element of K10(K10( the carrier of (TopSpaceMetr T)))

C is Element of K10( the carrier of (TopSpaceMetr T))

Cl C is Element of K10( the carrier of (TopSpaceMetr T))

x is set

meet x is set

bool the carrier of (TopSpaceMetr T) is non empty Element of K10(K10( the carrier of (TopSpaceMetr T)))

z is set

n is set

x9 is Element of K10( the carrier of (TopSpaceMetr T))

x9 is Element of K10( the carrier of (TopSpaceMetr T))

Cl x9 is Element of K10( the carrier of (TopSpaceMetr T))

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

{ b

( B <= b

y is Element of K10( the carrier of (TopSpaceMetr T))

g is Element of K10( the carrier of (TopSpaceMetr T))

Cl g is Element of K10( the carrier of (TopSpaceMetr T))

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

{ b

( m <= b

g is set

x is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

g is set

x is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

z is set

n is Element of K10( the carrier of (TopSpaceMetr T))

x9 is Element of K10( the carrier of (TopSpaceMetr T))

Cl x9 is Element of K10( the carrier of (TopSpaceMetr T))

meet (clf B) is Element of K10( the carrier of (TopSpaceMetr T))

x is Element of the carrier of (TopSpaceMetr T)

z is Element of the carrier of T

n is ext-real V30() real Element of REAL

n / 2 is ext-real V30() real Element of REAL

x9 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

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

Ball (z,(n / 2)) is Element of K10( the carrier of T)

y is Element of K10( the carrier of (TopSpaceMetr T))

{ b

B is Element of K10( the carrier of (TopSpaceMetr T))

Cl B is Element of K10( the carrier of (TopSpaceMetr T))

B /\ y is Element of K10( the carrier of (TopSpaceMetr T))

g is set

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

A . m is Element of the carrier of T

dist ((A . m),z) is ext-real V30() real Element of REAL

g is Element of the carrier of T

x is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,A,n) is Element of the carrier of T

(T,A,m) is Element of the carrier of T

dist ((T,A,m),(T,A,n)) is ext-real V30() real Element of REAL

dist ((T,A,n),z) is ext-real V30() real Element of REAL

(n / 2) + (n / 2) is ext-real V30() real Element of REAL

(dist ((T,A,m),(T,A,n))) + (dist ((T,A,n),z)) is ext-real V30() real Element of REAL

dist ((T,A,m),z) is ext-real V30() real Element of REAL

T is non empty MetrStruct

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

A is ext-real V30() real Element of REAL

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

p is Element of K10(K10( the carrier of T))

Family_open_set T is Element of K10(K10( the carrier of T))

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

the carrier of (TopSpaceMetr T) is non empty set

K10( the carrier of (TopSpaceMetr T)) is non empty set

K10(K10( the carrier of (TopSpaceMetr T))) is non empty set

B is Element of K10(K10( the carrier of (TopSpaceMetr T)))

union B is Element of K10( the carrier of (TopSpaceMetr T))

C is Element of the carrier of (TopSpaceMetr T)

B is Element of the carrier of T

dist (B,B) is ext-real V30() real Element of REAL

Ball (B,A) is Element of K10( the carrier of T)

[#] (TopSpaceMetr T) is non empty non proper Element of K10( the carrier of (TopSpaceMetr T))

C is Element of K10( the carrier of (TopSpaceMetr T))

B is Element of K10( the carrier of T)

the topology of (TopSpaceMetr T) is Element of K10(K10( the carrier of (TopSpaceMetr T)))

C is Element of the carrier of T

Ball (C,A) is Element of K10( the carrier of T)

C is Element of K10(K10( the carrier of (TopSpaceMetr T)))

B is Element of K10(K10( the carrier of T))

union B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

T is non empty MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

T is non empty set

DiscreteSpace T is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of (DiscreteSpace T) is non empty set

A is Element of the carrier of (DiscreteSpace T)

p is Element of the carrier of (DiscreteSpace T)

dist (A,p) is ext-real V30() real Element of REAL

discrete_dist T is Relation-like K11(T,T) -defined REAL -valued Function-like V33(K11(T,T), REAL ) Element of K10(K11(K11(T,T),REAL))

K11(T,T) is non empty set

K11(K11(T,T),REAL) is non empty set

K10(K11(K11(T,T),REAL)) is non empty set

MetrStruct(# T,(discrete_dist T) #) is strict MetrStruct

dist (A,p) is ext-real V30() real Element of REAL

the distance of (DiscreteSpace T) is Relation-like K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)) -defined REAL -valued Function-like V33(K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)), REAL ) Element of K10(K11(K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)),REAL))

K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)) is non empty set

K11(K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)),REAL) is non empty set

K10(K11(K11( the carrier of (DiscreteSpace T), the carrier of (DiscreteSpace T)),REAL)) is non empty set

the distance of (DiscreteSpace T) . (A,p) is ext-real V30() real Element of REAL

{0} is non empty finite V40() V112() V113() V114() V115() V116() V117() Element of K10(NAT)

DiscreteSpace {0} is non empty strict Reflexive discerning symmetric triangle Discerning () MetrStruct

T is non empty MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

A is Element of the carrier of T

p is Element of the carrier of T

dist (A,p) is ext-real V30() real Element of REAL

T is non empty MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

{} T is empty proper functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() (T) Element of K10( the carrier of T)

T is non empty MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

the Element of S1 is Element of S1

B is ext-real V30() real Element of REAL

p is Element of the carrier of T

C is Element of the carrier of T

dist (p,C) is ext-real V30() real Element of REAL

A is ext-real V30() real Element of REAL

p is Element of the carrier of T

A + A is ext-real V30() real Element of REAL

C is symmetric MetrStruct

the carrier of C is set

C is Element of the carrier of C

x is Element of the carrier of C

dist (C,x) is ext-real V30() real Element of REAL

B is Element of the carrier of C

dist (B,C) is ext-real V30() real Element of REAL

dist (B,x) is ext-real V30() real Element of REAL

dist (C,B) is ext-real V30() real Element of REAL

(dist (C,B)) + (dist (B,x)) is ext-real V30() real Element of REAL

C is ext-real V30() real Element of REAL

T is non empty MetrStruct

the carrier of T is non empty set

S1 is Element of the carrier of T

A is ext-real V30() real set

Ball (S1,A) is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

dist (S1,S1) is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

S1 is Element of the carrier of T

A is ext-real V30() real set

Ball (S1,A) is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

the Element of Ball (S1,A) is Element of Ball (S1,A)

B is Element of the carrier of T

dist (S1,B) is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

S1 is Element of the carrier of T

A is ext-real V30() real set

Ball (S1,A) is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

B is ext-real V30() real Element of REAL

C is Element of the carrier of T

dist (S1,C) is ext-real V30() real Element of REAL

C is ext-real V30() real Element of REAL

B is Element of the carrier of T

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

S1 is Element of the carrier of T

A is ext-real V30() real set

Ball (S1,A) is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

{} T is empty proper functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() (T) Element of K10( the carrier of T)

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

S1 \/ A is Element of K10( the carrier of T)

p is ext-real V30() real Element of REAL

B is Element of the carrier of T

C is ext-real V30() real Element of REAL

B is Element of the carrier of T

C + p is ext-real V30() real Element of REAL

dist (B,B) is ext-real V30() real Element of REAL

(C + p) + (dist (B,B)) is ext-real V30() real Element of REAL

(dist (B,B)) + p is ext-real V30() real Element of REAL

C + ((dist (B,B)) + p) is ext-real V30() real Element of REAL

x is Element of the carrier of T

dist (B,x) is ext-real V30() real Element of REAL

dist (B,x) is ext-real V30() real Element of REAL

(dist (B,B)) + (dist (B,x)) is ext-real V30() real Element of REAL

dist (B,x) is ext-real V30() real Element of REAL

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

z is Element of the carrier of T

T is non empty MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

p is ext-real V30() real Element of REAL

B is Element of the carrier of T

C is Element of the carrier of T

dist (B,C) is ext-real V30() real Element of REAL

B is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of the carrier of T

{S1} is non empty finite Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

Ball (S1,1) is (T) Element of K10( the carrier of T)

K10((Ball (S1,1))) is non empty set

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

{} T is empty proper functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() (T) Element of K10( the carrier of T)

A is set

p is set

{A} is non empty finite set

p \/ {A} is non empty set

B is Element of the carrier of T

{B} is non empty finite Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

p \/ {B} is non empty set

B \/ C is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

the non empty finite (T) Element of K10( the carrier of T) is non empty finite (T) Element of K10( the carrier of T)

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

S1 is Element of K10(K10( the carrier of T))

union S1 is Element of K10( the carrier of T)

A is set

p is set

union p is set

{A} is non empty finite set

p \/ {A} is non empty set

union (p \/ {A}) is set

B is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

{C} is non empty finite Element of K10(K10( the carrier of T))

p \/ {C} is non empty set

union (p \/ {C}) is set

union {C} is Element of K10( the carrier of T)

(union p) \/ (union {C}) is set

(union p) \/ C is set

B \/ C is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

{} T is empty proper functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real finite V40() FinSequence-membered V112() V113() V114() V115() V116() V117() V118() (T) Element of K10( the carrier of T)

union S1 is set

A is Element of K10( the carrier of T)

T is non empty MetrStruct

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is ext-real V30() real Element of REAL

A is Element of the carrier of T

p is Element of the carrier of T

dist (A,p) is ext-real V30() real Element of REAL

S1 is ext-real V30() real Element of REAL

A is Element of the carrier of T

p is Element of the carrier of T

dist (A,p) is ext-real V30() real Element of REAL

T is non empty () MetrStruct

[#] T is non empty non proper Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

S1 is Element of K10(K10( the carrier of T))

union S1 is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

p is Element of the carrier of T

Ball (p,1) is (T) Element of K10( the carrier of T)

[#] T is non empty non proper Element of K10( the carrier of T)

T is non empty Reflexive MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

the Element of S1 is Element of S1

{ b

{ b

C is ext-real V30() real set

B is ext-real V30() real set

C is ext-real V30() real Element of REAL

x is Element of the carrier of T

z is Element of the carrier of T

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

n is ext-real V30() real Element of REAL

C is Element of the carrier of T

dist (C,C) is ext-real V30() real Element of REAL

C is ext-real V30() real Element of REAL

B is V112() V113() V114() Element of K10(REAL)

x is V112() V113() V114() Element of K10(REAL)

z is ext-real V30() real set

n is Element of the carrier of T

x9 is Element of the carrier of T

dist (n,x9) is ext-real V30() real Element of REAL

n is ext-real V30() real Element of REAL

A is ext-real V30() real Element of REAL

p is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is set

{S1} is non empty finite set

A is Element of K10( the carrier of T)

(T,A) is ext-real V30() real Element of REAL

B is Element of the carrier of T

C is Element of the carrier of T

dist (B,C) is ext-real V30() real Element of REAL

p is Element of the carrier of T

dist (p,p) is ext-real V30() real Element of REAL

B is ext-real V30() real Element of REAL

p is Element of the carrier of T

dist (p,p) is ext-real V30() real Element of REAL

T is non empty Reflexive MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

(T,S1) is ext-real V30() real Element of REAL

the Element of S1 is Element of S1

p is Element of the carrier of T

dist (p,p) is ext-real V30() real Element of REAL

T is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

(T,S1) is ext-real V30() real Element of REAL

the Element of S1 is Element of S1

p is Element of the carrier of T

{p} is non empty finite (T) Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of the carrier of T

dist (C,p) is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

S1 is Element of the carrier of T

A is ext-real V30() real Element of REAL

Ball (S1,A) is (T) Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

(T,(Ball (S1,A))) is ext-real V30() real Element of REAL

2 * A is ext-real V30() real Element of REAL

p is Element of the carrier of T

B is Element of the carrier of T

dist (p,B) is ext-real V30() real Element of REAL

dist (S1,p) is ext-real V30() real Element of REAL

dist (S1,B) is ext-real V30() real Element of REAL

A + A is ext-real V30() real Element of REAL

(dist (S1,p)) + (dist (S1,B)) is ext-real V30() real Element of REAL

dist (p,S1) is ext-real V30() real Element of REAL

(dist (p,S1)) + (dist (S1,B)) is ext-real V30() real Element of REAL

T is non empty Reflexive MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

(T,A) is ext-real V30() real Element of REAL

(T,S1) is ext-real V30() real Element of REAL

p is Element of the carrier of T

B is Element of the carrier of T

dist (p,B) is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

S1 is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

S1 \/ A is Element of K10( the carrier of T)

(T,(S1 \/ A)) is ext-real V30() real Element of REAL

(T,S1) is ext-real V30() real Element of REAL

(T,A) is ext-real V30() real Element of REAL

(T,S1) + (T,A) is ext-real V30() real Element of REAL

S1 /\ A is Element of K10( the carrier of T)

the Element of S1 /\ A is Element of S1 /\ A

x is Element of the carrier of T

z is Element of the carrier of T

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

C is Element of the carrier of T

dist (x,C) is ext-real V30() real Element of REAL

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

(dist (x,C)) + (dist (C,z)) is ext-real V30() real Element of REAL

(T,A) + (T,S1) is ext-real V30() real Element of REAL

T is non empty Reflexive symmetric triangle MetrStruct

the carrier of T is non empty set

K11(NAT, the carrier of T) is non empty set

K10(K11(NAT, the carrier of T)) is non empty set

S1 is Relation-like NAT -defined the carrier of T -valued Function-like V33( NAT , the carrier of T) Element of K10(K11(NAT, the carrier of T))

rng S1 is Element of K10( the carrier of T)

K10( the carrier of T) is non empty set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

{ b

{ b

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

Seg p is finite V43(p) V112() V113() V114() V115() V116() V117() Element of K10(NAT)

{0} is non empty finite V40() V112() V113() V114() V115() V116() V117() Element of K10(NAT)

{0} \/ (Seg p) is non empty finite V112() V113() V114() V115() V116() V117() Element of K10(NAT)

n is set

S1 .: ({0} \/ (Seg p)) is finite (T) Element of K10( the carrier of T)

x9 is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

x9 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real set

x9 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

{ b

dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

x9 is set

S1 . x9 is set

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

x9 is Element of the carrier of T

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,B) is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

{ b

x9 is Element of the carrier of T

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,B) is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

B is Element of K10( the carrier of T)

B \/ C is Element of K10( the carrier of T)

x is set

dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

z is set

S1 . z is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,n) is Element of the carrier of T

x9 is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

x9 is Element of the carrier of T

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,y) is Element of the carrier of T

x is set

z is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,n) is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,n) is Element of the carrier of T

dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

z is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,n) is Element of the carrier of T

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,n) is Element of the carrier of T

dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

(T,S1,p) is Element of the carrier of T

z is Element of the carrier of T

dist ((T,S1,p),z) is ext-real V30() real Element of REAL

n is Element of the carrier of T

x9 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT

(T,S1,x9) is Element of the carrier of T

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

n is Element of the carrier of T