:: 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₁ where b₁ is Element of the carrier of T : ex b₂ 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 <= b₂ & b₁ = (T,A,b₂) ) } is set
(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₁ where b₁ is Element of the carrier of T : S₂[b₁] } is set
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₁ where b₁ is Element of the carrier of T : ex b₂ 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 <= b₂ & b₁ = (T,A,b₂) ) } is set
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₁ where b₁ is Element of the carrier of T : ex b₂ 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 <= b₂ & b₁ = (T,A,b₂) ) } is set
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₁ where b₁ is Element of the carrier of T : S₃[b₁] } is set
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₁ where b₁ is ext-real V30() real Element of REAL : S₁[b₁] } is set
{ b₁ where b₁ is ext-real V30() real Element of REAL : S₂[b₁] } 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
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₁ where b₁ is Element of the carrier of T : S₁[b₁] } is set
{ b₁ where b₁ is Element of the carrier of T : S₂[b₁] } 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)
{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₁ where 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 : ( 1 <= b₁ & b₁ <= p ) } is set
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₁ where 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 : ( 1 <= b₁ & b₁ <= p ) } is set
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