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

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

K11(NAT,REAL) is non empty set
K10(K11(NAT,REAL)) is non empty 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

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

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

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 is ext-real V30() real Element of REAL
S1 is ext-real V30() real Element of REAL

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

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

dom S1 is set

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

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

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

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

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

(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

S1 . B is Element of the carrier of T

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

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

(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

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

(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

(dist ((T,p,1),(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

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

1 - () 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 - ()) / (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

(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

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

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

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

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

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

(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

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

(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

((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 + 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

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

{ b1 where b1 is Element of the carrier of T : ex b2 being ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT st
( p <= b2 & b1 = (T,A,b2) )
}
is set

(T,A,p) is Element of the carrier of T
the carrier of () is non empty set
K10( the carrier of ()) is non empty set
K10(K10( the carrier of ())) is non empty set
p is Element of K10(K10( the carrier of ()))
{ b1 where b1 is Element of the carrier of T : S2[b1] } is set
B is Element of K10(K10( the carrier of ()))
clf B is Element of K10(K10( the carrier of ()))
C is Element of K10( the carrier of ())
Cl C is Element of K10( the carrier of ())
x is set
meet x is set
bool the carrier of () is non empty Element of K10(K10( the carrier of ()))
z is set
n is set
x9 is Element of K10( the carrier of ())
x9 is Element of K10( the carrier of ())
Cl x9 is Element of K10( the carrier of ())

{ b1 where b1 is Element of the carrier of T : ex b2 being ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT st
( B <= b2 & b1 = (T,A,b2) )
}
is set

y is Element of K10( the carrier of ())
g is Element of K10( the carrier of ())
Cl g is Element of K10( the carrier of ())

{ b1 where b1 is Element of the carrier of T : ex b2 being ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT st
( m <= b2 & b1 = (T,A,b2) )
}
is set

g is set
x is Element of the carrier of T

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

(T,A,n) is Element of the carrier of T
g is set
x is Element of the carrier of T

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

(T,A,n) is Element of the carrier of T
z is set
n is Element of K10( the carrier of ())
x9 is Element of K10( the carrier of ())
Cl x9 is Element of K10( the carrier of ())
meet (clf B) is Element of K10( the carrier of ())
x is Element of the carrier of ()
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

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 ())
{ b1 where b1 is Element of the carrier of T : S3[b1] } is set
B is Element of K10( the carrier of ())
Cl B is Element of K10( the carrier of ())
B /\ y is Element of K10( the carrier of ())
g is set

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

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

(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

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,() #) is strict TopStruct
the carrier of () is non empty set
K10( the carrier of ()) is non empty set
K10(K10( the carrier of ())) is non empty set
B is Element of K10(K10( the carrier of ()))
union B is Element of K10( the carrier of ())
C is Element of the carrier of ()
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)
[#] () is non empty non proper Element of K10( the carrier of ())
C is Element of K10( the carrier of ())
B is Element of K10( the carrier of T)
the topology of () is Element of K10(K10( the carrier of ()))
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 ()))
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

the carrier of () is non empty set
A is Element of the carrier of ()
p is Element of the carrier of ()
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,() #) is strict MetrStruct
dist (A,p) is ext-real V30() real Element of REAL
the distance of () is Relation-like K11( the carrier of (), the carrier of ()) -defined REAL -valued Function-like V33(K11( the carrier of (), the carrier of ()), REAL ) Element of K10(K11(K11( the carrier of (), the carrier of ()),REAL))
K11( the carrier of (), the carrier of ()) is non empty set
K11(K11( the carrier of (), the carrier of ()),REAL) is non empty set
K10(K11(K11( the carrier of (), the carrier of ()),REAL)) is non empty set
the distance of () . (A,p) is ext-real V30() real Element of REAL
is non empty finite V40() V112() V113() V114() V115() V116() V117() Element of K10(NAT)

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

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

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

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

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

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

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

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

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)
() \/ () is set
() \/ C is set
B \/ C is Element of K10( the carrier of T)
B is 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

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
{ b1 where b1 is ext-real V30() real Element of REAL : S1[b1] } is set
{ b1 where b1 is ext-real V30() real Element of REAL : S2[b1] } is set
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

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

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

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

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

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

{ b1 where b1 is Element of the carrier of T : S1[b1] } is set
{ b1 where b1 is Element of the carrier of T : S2[b1] } is set
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)
is non empty finite V40() V112() V113() V114() V115() V116() V117() Element of K10(NAT)
\/ (Seg p) is non empty finite V112() V113() V114() V115() V116() V117() Element of K10(NAT)
n is set
S1 .: ( \/ (Seg p)) is finite (T) Element of K10( the carrier of T)
x9 is Element of the carrier of T

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

(T,S1,y) is Element of the carrier of T
dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)

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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set
dom S1 is V112() V113() V114() V115() V116() V117() Element of K10(NAT)
x9 is set
S1 . x9 is set

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

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

(T,S1,y) is Element of the carrier of T
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set
x9 is Element of the carrier of T

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

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

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

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

(T,S1,y) is Element of the carrier of T
x is set
z is Element of the carrier of T

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

(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

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

(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

(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