:: TBSP_1 semantic presentation

begin

theorem :: TBSP_1:1
for L being ( ( ) ( ext-real V30() real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < L : ( ( ) ( ext-real V30() real ) Real) & L : ( ( ) ( ext-real V30() real ) Real) < 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
for n, m being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
L : ( ( ) ( ext-real V30() real ) Real) to_power m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= L : ( ( ) ( ext-real V30() real ) Real) to_power n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ;

theorem :: TBSP_1:2
for L being ( ( ) ( ext-real V30() real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < L : ( ( ) ( ext-real V30() real ) Real) & L : ( ( ) ( ext-real V30() real ) Real) < 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
for k being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
( L : ( ( ) ( ext-real V30() real ) Real) to_power k : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < L : ( ( ) ( ext-real V30() real ) Real) to_power k : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) ;

theorem :: TBSP_1:3
for L being ( ( ) ( ext-real V30() real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < L : ( ( ) ( ext-real V30() real ) Real) & L : ( ( ) ( ext-real V30() real ) Real) < 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
for s being ( ( ) ( ext-real V30() real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < s : ( ( ) ( ext-real V30() real ) Real) holds
ex n being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st L : ( ( ) ( ext-real V30() real ) Real) to_power n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) < s : ( ( ) ( ext-real V30() real ) Real) ;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr N is totally_bounded means :: TBSP_1:def 1
 for r being ( ( ) ( ext-real V30() real ) Real) st r : ( ( ) ( ext-real V30() real ) Real) > 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex G being ( ( ) ( ) Subset-Family of ) st
( G : ( ( ) ( ) Subset-Family of ) is finite & the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) = union G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for C being ( ( ) ( ) Subset of ) st C : ( ( ) ( ) Subset of ) in G : ( ( ) ( ) Subset-Family of ) holds
ex w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st C : ( ( ) ( ) Subset of ) = Ball (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ext-real V30() real ) Real) ) : ( ( ) ( ) Element of K10( the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: TBSP_1:4
for N being ( ( non empty ) ( non empty ) MetrStruct )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) iff ( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for n being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
let S2 be ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
attr S2 is convergent means :: TBSP_1:def 2
 ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
for r being ( ( ) ( ext-real V30() real ) Real) st r : ( ( ) ( ext-real V30() real ) Real) > 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex n being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st
for m being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
dist ((S2 : ( ( Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) ( Relation-like K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) -valued Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) Element of K10(K11(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) < r : ( ( ) ( ext-real V30() real ) Real) ;
end;

definition
let M be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
let S1 be ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
assume S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;
func lim S1 -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: TBSP_1:def 3
 for r being ( ( ) ( ext-real V30() real ) Real) st r : ( ( ) ( ext-real V30() real ) Real) > 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex n being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st
for m being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
dist ((S1 : ( ( Function-like V33(K11(M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) ( Relation-like K11(M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) -valued Function-like V33(K11(M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) Element of K10(K11(K11(M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,it : ( ( ) ( ) Element of M : ( ( ) ( ) MetrStruct ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) < r : ( ( ) ( ext-real V30() real ) Real) ;
end;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
let S2 be ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
attr S2 is Cauchy means :: TBSP_1:def 4
 for r being ( ( ) ( ext-real V30() real ) Real) st r : ( ( ) ( ext-real V30() real ) Real) > 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex p being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st
for n, m being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & p : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
dist ((S2 : ( ( Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) ( Relation-like K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) -valued Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) Element of K10(K11(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,(S2 : ( ( Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) ( Relation-like K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) -valued Function-like V33(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ) Element of K10(K11(K11(N : ( ( ) ( ) MetrStruct ) ,N : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . m : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) < r : ( ( ) ( ext-real V30() real ) Real) ;
end;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr N is complete means :: TBSP_1:def 5
 for S2 being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) st S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy holds
S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;
end;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
let S2 be ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let n be ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: .
redefine func S2 . n -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

theorem :: TBSP_1:5
for N being ( ( non empty ) ( non empty ) MetrStruct )
for S2 being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st N : ( ( non empty ) ( non empty ) MetrStruct ) is triangle & N : ( ( non empty ) ( non empty ) MetrStruct ) is symmetric & S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy ;

registration
let M be ( ( non empty symmetric triangle ) ( non empty symmetric triangle ) MetrStruct ) ;
cluster Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) convergent -> Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) Cauchy for ( ( ) ( ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: TBSP_1:6
for N being ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct )
for S2 being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy iff for r being ( ( ) ( ext-real V30() real ) Real) st r : ( ( ) ( ext-real V30() real ) Real) > 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex p being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st
for n, k being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
dist ((S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . (n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) + k : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(S2 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty symmetric ) ( non empty symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V30() real V110() V111() V112() V113() V114() V115() V116() V117() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) < r : ( ( ) ( ext-real V30() real ) Real) ) ;

theorem :: TBSP_1:7
for M being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for f being ( ( Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) ( Relation-like the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) Contraction of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ) st M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) is complete holds
ex c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) ( Relation-like the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) Contraction of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ) . c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) ( Relation-like the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) contraction ) Contraction of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ) . y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: TBSP_1:8
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) st TopSpaceMetr T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) is compact holds
T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) is complete ;

theorem :: TBSP_1:9
for N being ( ( non empty ) ( non empty ) MetrStruct ) st N : ( ( non empty ) ( non empty ) MetrStruct ) is Reflexive & N : ( ( non empty ) ( non empty ) MetrStruct ) is triangle & TopSpaceMetr N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) is compact holds
N : ( ( non empty ) ( non empty ) MetrStruct ) is totally_bounded ;

definition
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr N is bounded means :: TBSP_1:def 6
 ex r being ( ( ) ( ext-real V30() real ) Real) st
( 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( ext-real V30() real ) Real) & ( for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds dist (x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= r : ( ( ) ( ext-real V30() real ) Real) ) );
let C be ( ( ) ( ) Subset of ) ;
attr C is bounded means :: TBSP_1:def 7
 ex r being ( ( ) ( ext-real V30() real ) Real) st
( 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( ext-real V30() real ) Real) & ( for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) holds
dist (x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= r : ( ( ) ( ext-real V30() real ) Real) ) );
end;

registration
let A be ( ( non empty ) ( non empty ) set ) ;
cluster DiscreteSpace A : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrStruct ) -> strict bounded ;
end;

registration
cluster non empty Reflexive discerning symmetric triangle Discerning bounded for ( ( ) ( ) MetrStruct ) ;
end;

registration
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster empty -> bounded for ( ( ) ( ) Element of K10( the carrier of N : ( ( V41() ) ( V41() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let N be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster bounded for ( ( ) ( ) Element of K10( the carrier of N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: TBSP_1:10
for N being ( ( non empty ) ( non empty ) MetrStruct )
for C being ( ( ) ( ) Subset of ) holds
( ( C : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( 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 ) & C : ( ( ) ( ) Subset of ) is bounded implies ex r being ( ( ) ( ext-real V30() real ) Real) ex w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( ext-real V30() real ) Real) & w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Subset of ) & ( for z being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Subset of ) holds
dist (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= r : ( ( ) ( ext-real V30() real ) Real) ) ) ) & ( N : ( ( non empty ) ( non empty ) MetrStruct ) is symmetric & N : ( ( non empty ) ( non empty ) MetrStruct ) is triangle & ex r being ( ( ) ( ext-real V30() real ) Real) ex w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( ext-real V30() real ) Real) & ( for z being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Subset of ) holds
dist (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= r : ( ( ) ( ext-real V30() real ) Real) ) ) implies C : ( ( ) ( ) Subset of ) is bounded ) ) ;

theorem :: TBSP_1:11
for N being ( ( non empty ) ( non empty ) MetrStruct )
for w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for r being ( ( real ) ( ext-real V30() real ) number ) st N : ( ( non empty ) ( non empty ) MetrStruct ) is Reflexive & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( real ) ( ext-real V30() real ) number ) holds
w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Ball (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V30() real ) number ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TBSP_1:12
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for t1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for r being ( ( real ) ( ext-real V30() real ) number ) st r : ( ( real ) ( ext-real V30() real ) number ) <= 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
Ball (t1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V30() real ) number ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( 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 ) ;

registration
let T be ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) ;
let t1 be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let r be ( ( real ) ( ext-real V30() real ) number ) ;
cluster Ball (t1 : ( ( ) ( ) Element of the carrier of T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V30() real ) set ) ) : ( ( ) ( ) Element of K10( the carrier of T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> bounded ;
end;

theorem :: TBSP_1:13
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for P, Q being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) is bounded & Q : ( ( ) ( ) Subset of ) is bounded holds
P : ( ( ) ( ) Subset of ) \/ Q : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is bounded ;

theorem :: TBSP_1:14
for N being ( ( non empty ) ( non empty ) MetrStruct )
for C, D being ( ( ) ( ) Subset of ) st C : ( ( ) ( ) Subset of ) is bounded & D : ( ( ) ( ) Subset of ) c= C : ( ( ) ( ) Subset of ) holds
D : ( ( ) ( ) Subset of ) is bounded ;

theorem :: TBSP_1:15
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for t1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = {t1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
P : ( ( ) ( ) Subset of ) is bounded ;

theorem :: TBSP_1:16
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) is finite holds
P : ( ( ) ( ) Subset of ) is bounded ;

registration
let T be ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) ;
cluster finite -> bounded for ( ( ) ( ) Element of K10( the carrier of T : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) ;
cluster non empty finite for ( ( ) ( ) Element of K10( the carrier of T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: TBSP_1:17
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for Y being ( ( ) ( ) Subset-Family of ) st Y : ( ( ) ( ) Subset-Family of ) is finite & ( for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) in Y : ( ( ) ( ) Subset-Family of ) holds
P : ( ( ) ( ) Subset of ) is bounded ) holds
union Y : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is bounded ;

theorem :: TBSP_1:18
for N being ( ( non empty ) ( non empty ) MetrStruct ) holds
( N : ( ( non empty ) ( non empty ) MetrStruct ) is bounded iff [#] N : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty non proper ) Element of K10( the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is bounded ) ;

registration
let N be ( ( non empty bounded ) ( non empty bounded ) MetrStruct ) ;
cluster [#] N : ( ( non empty bounded ) ( non empty bounded ) MetrStruct ) : ( ( ) ( non empty non proper ) Element of K10( the carrier of N : ( ( non empty bounded ) ( non empty bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> bounded ;
end;

theorem :: TBSP_1:19
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) st T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) is totally_bounded holds
T : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) is bounded ;

definition
let N be ( ( non empty Reflexive ) ( non empty Reflexive ) MetrStruct ) ;
let C be ( ( ) ( ) Subset of ) ;
assume C : ( ( ) ( ) Subset of ) is bounded ;
func diameter C -> ( ( ) ( ext-real V30() real ) Real) means :: TBSP_1:def 8
( ( for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ext-real V30() real ) Real) in C : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) holds
dist (x : ( ( ) ( ext-real V30() real ) Real) ,y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= it : ( ( real ) ( ext-real V30() real ) set ) ) & ( for s being ( ( ) ( ext-real V30() real ) Real) st ( for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) holds
dist (x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) <= s : ( ( ) ( ext-real V30() real ) Real) ) holds
it : ( ( real ) ( ext-real V30() real ) set ) <= s : ( ( ) ( ext-real V30() real ) Real) ) ) if C : ( ( non empty ) ( non empty ) set ) <> {} : ( ( ) ( 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 )
otherwise it : ( ( real ) ( ext-real V30() real ) set ) = 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: TBSP_1:20
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for x being ( ( ) ( ) set )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) holds
diameter P : ( ( ) ( ) Subset of ) : ( ( ) ( ext-real V30() real ) Real) = 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TBSP_1:21
for R being ( ( non empty Reflexive ) ( non empty Reflexive ) MetrStruct )
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) is bounded holds
0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= diameter S : ( ( ) ( ) Subset of ) : ( ( ) ( ext-real V30() real ) Real) ;

theorem :: TBSP_1:22
for M being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( 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 ) & A : ( ( ) ( ) Subset of ) is bounded & diameter A : ( ( ) ( ) Subset of ) : ( ( ) ( ext-real V30() real ) Real) = 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
ex g being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ) = {g : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite bounded ) Element of K10( the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TBSP_1:23
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for t1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for r being ( ( ) ( ext-real V30() real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( ext-real V30() real ) Real) holds
diameter (Ball (t1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ext-real V30() real ) Real) )) : ( ( ) ( bounded ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V30() real ) Real) <= 2 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) ) * r : ( ( ) ( ext-real V30() real ) Real) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ;

theorem :: TBSP_1:24
for R being ( ( non empty Reflexive ) ( non empty Reflexive ) MetrStruct )
for S, V being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) is bounded & V : ( ( ) ( ) Subset of ) c= S : ( ( ) ( ) Subset of ) holds
diameter V : ( ( ) ( ) Subset of ) : ( ( ) ( ext-real V30() real ) Real) <= diameter S : ( ( ) ( ) Subset of ) : ( ( ) ( ext-real V30() real ) Real) ;

theorem :: TBSP_1:25
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for P, Q being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) is bounded & Q : ( ( ) ( ) Subset of ) is bounded & P : ( ( ) ( ) Subset of ) meets Q : ( ( ) ( ) Subset of ) holds
diameter (P : ( ( ) ( ) Subset of ) \/ Q : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V30() real ) Real) <= (diameter P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ext-real V30() real ) Real) + (diameter Q : ( ( ) ( ) Subset of ) ) : ( ( ) ( ext-real V30() real ) Real) : ( ( ) ( ext-real V30() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) ;

theorem :: TBSP_1:26
for T being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for S1 being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy holds
rng S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V112() V113() V114() V115() V116() V117() V118() ) Element of K10(REAL : ( ( ) ( non empty non trivial non finite V112() V113() V114() V118() ) set ) ) : ( ( ) ( non empty ) set ) ) , the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is bounded ;