:: METRIC_6 semantic presentation

begin

theorem :: METRIC_6:1
for X being ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrSpace)
for x, z, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds abs ((dist (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) - (dist (y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) <= dist (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;

theorem :: METRIC_6:2
for A being ( ( non empty ) ( non empty ) set )
for G being ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) st G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is_metric_of A : ( ( non empty ) ( non empty ) set ) holds
for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) <= G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;

theorem :: METRIC_6:3
for A being ( ( non empty ) ( non empty ) set )
for G being ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) holds
( G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is_metric_of A : ( ( non empty ) ( non empty ) set ) iff ( G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is Reflexive & G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is discerning & G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is symmetric & G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is triangle ) ) ;

theorem :: METRIC_6:4
for X being ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) holds
( the distance of X : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( Function-like V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is Reflexive & the distance of X : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( Function-like V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is discerning & the distance of X : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( Function-like V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is symmetric & the distance of X : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( Function-like V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[: the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is triangle ) ;

theorem :: METRIC_6:5
for A being ( ( non empty ) ( non empty ) set )
for G being ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) holds
( G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is_metric_of A : ( ( non empty ) ( non empty ) set ) iff ( G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is Reflexive & G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is discerning & ( for a, b, c being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) <= (G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) + (G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ) ) ) ;

definition
let A be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( Function-like V30([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ;
func bounded_metric (A,G) -> ( ( Function-like V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) means :: METRIC_6:def 1
 for a, b being ( ( ) ( ) Element of A : ( ( ) ( ) MetrStruct ) ) holds it : ( ( ) ( ) Element of A : ( ( ) ( ) MetrStruct ) ) . (a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) = (G : ( ( Function-like V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) / (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) + (G : ( ( Function-like V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;
end;

theorem :: METRIC_6:6
for A being ( ( non empty ) ( non empty ) set )
for G being ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) st G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is_metric_of A : ( ( non empty ) ( non empty ) set ) holds
bounded_metric (A : ( ( non empty ) ( non empty ) set ) ,G : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) : ( ( Function-like V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V30([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) is_metric_of A : ( ( non empty ) ( non empty ) set ) ;

theorem :: METRIC_6:7
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st rng S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) ;

definition
let X be ( ( non empty ) ( non empty ) MetrStruct ) ;
let S be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred S is_convergent_in_metrspace_to x means :: METRIC_6:def 2
 for r being ( ( ) ( V24() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) holds
ex m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) st m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) holds
dist ((S : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V24() real ext-real ) Element of the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) < r : ( ( ) ( V24() real ext-real ) Real) ;
end;

definition
let X be ( ( non empty symmetric triangle ) ( non empty symmetric triangle ) MetrStruct ) ;
let V be ( ( ) ( ) Subset of ) ;
redefine attr V is bounded means :: METRIC_6:def 3
 ex r being ( ( ) ( V24() real ext-real ) Real) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) & V : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) c= Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

definition
let X be ( ( non empty ) ( non empty ) MetrStruct ) ;
let S be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
attr S is bounded means :: METRIC_6:def 4
 ex r being ( ( ) ( V24() real ext-real ) Real) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) & rng S : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V106() V107() V108() ) set ) c= Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

definition
let X be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
let V be ( ( ) ( ) Subset of ) ;
let S be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
pred V contains_almost_all_sequence S means :: METRIC_6:def 5
 ex m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) st m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) holds
S : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) in V : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: METRIC_6:8
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is bounded iff ex r being ( ( ) ( V24() real ext-real ) Real) ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) in Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( bounded ) Element of bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: METRIC_6:9
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: METRIC_6:10
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
let S be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func dist_to_point (S,x) -> ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) means :: METRIC_6:def 6
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) = dist ((S : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V24() real ext-real ) Element of the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;
end;

definition
let X be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
let S, T be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
func sequence_of_dist (S,T) -> ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) means :: METRIC_6:def 7
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) = dist ((S : ( ( Function-like V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ) V30([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V45() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V24() real ext-real ) Element of the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,(T : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V24() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;
end;

theorem :: METRIC_6:11
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
lim S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence 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 ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_6:12
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff ( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & lim S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence 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 ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: METRIC_6:13
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & lim S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence 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 ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: METRIC_6:14
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff ( dist_to_point (S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim (dist_to_point (S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: METRIC_6:15
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for r being ( ( ) ( V24() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) holds
Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( bounded ) Element of bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_6:16
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ( for r being ( ( ) ( V24() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( ) Subset of ) holds
Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) holds
for V being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) in Family_open_set X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
V : ( ( ) ( ) Subset of ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_6:17
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ( for V being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) in Family_open_set X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
V : ( ( ) ( ) Subset of ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_6:18
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for r being ( ( ) ( V24() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) holds
Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( bounded ) Element of bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) ;

theorem :: METRIC_6:19
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for V being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) in Family_open_set X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
V : ( ( ) ( ) Subset of ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) ;

theorem :: METRIC_6:20
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds
( ( for r being ( ( ) ( V24() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( ) Subset of ) holds
Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) iff for V being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( ) ( ) Subset of ) & V : ( ( ) ( ) Subset of ) in Family_open_set X : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( ) Element of bool (bool the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
V : ( ( ) ( ) Subset of ) contains_almost_all_sequence S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) ;

theorem :: METRIC_6:21
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S, T being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & T : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
dist ((lim S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence 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 ) ) ,(lim T : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence 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 ) ) ) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) = lim (sequence_of_dist (S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ,T : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() ) set ) -valued Function-like V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V45() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V24() real ext-real ) Element of REAL : ( ( ) ( non empty V45() ) set ) ) ;

theorem :: METRIC_6:22
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is_convergent_in_metrspace_to y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_6:23
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is constant holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: METRIC_6:24
errorfrm ;

theorem :: METRIC_6:25
errorfrm ;

theorem :: METRIC_6:26
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is constant holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy ;

theorem :: METRIC_6:27
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is bounded ;

theorem :: METRIC_6:28
for X being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy holds
S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( 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 ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is bounded ;

registration
let M be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
cluster Function-like constant V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) -> Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) convergent for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
cluster Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) Cauchy -> Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) bounded for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) ;
cluster non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like constant V29( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) ) convergent Cauchy bounded for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) , the carrier of M : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: METRIC_6:29
for X being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for V being ( ( bounded ) ( bounded ) Subset of )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex r being ( ( ) ( V24() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V45() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V24() real ext-real ) Real) & V : ( ( bounded ) ( bounded ) Subset of ) c= Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V24() real ext-real ) Real) ) : ( ( ) ( bounded ) Element of bool the carrier of b1 : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;