:: TOPMETR3 semantic presentation

begin

theorem :: TOPMETR3:1
for X being ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace)
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) )
for F being ( ( ) ( ) Subset of ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset of ) ) & F : ( ( ) ( ) Subset of ) is closed holds
lim S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset of ) ;

theorem :: TOPMETR3:2
for X, Y being ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

theorem :: TOPMETR3:3
for X, Y being ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) )
for T being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & T : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
T : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: TOPMETR3:4
for s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence)
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) st s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) = S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) holds
( ( s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent implies S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) is convergent ) & ( S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) is convergent implies s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent ) & ( s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent implies lim s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) = lim S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ) ;

theorem :: TOPMETR3:5
for a, b being ( ( real ) ( V11() real ext-real ) number )
for s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) st rng s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V168() V169() V170() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) c= [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V168() V169() V170() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) holds
s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

theorem :: TOPMETR3:6
for a, b being ( ( real ) ( V11() real ext-real ) number )
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) ;

theorem :: TOPMETR3:7
for a, b being ( ( real ) ( V11() real ext-real ) number )
for S1 being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) = S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
( ( S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) is convergent implies S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ) & ( S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent implies S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) is convergent ) & ( S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) is convergent implies lim S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) V158() V159() V160() ) sequence of ( ( ) ( non empty V168() V169() V170() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) : ( ( ) ( non empty V168() V169() V170() ) set ) ) = lim S1 : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: TOPMETR3:8
for a, b being ( ( real ) ( V11() real ext-real ) number )
for s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence)
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) = s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) & a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent holds
( S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & lim s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) = lim S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TOPMETR3:9
for a, b being ( ( real ) ( V11() real ext-real ) number )
for s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence)
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) = s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) & a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is non-decreasing holds
S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: TOPMETR3:10
for a, b being ( ( real ) ( V11() real ext-real ) number )
for s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence)
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) = s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) & a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is non-increasing holds
S : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of (Closed-Interval-MSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V86() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V86() triangle Discerning V116() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: TOPMETR3:11
for R being ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) st R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) is bounded_above holds
ex s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) st
( s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is non-decreasing & s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent & rng s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V168() V169() V170() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) c= R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) & lim s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) = upper_bound R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ;

theorem :: TOPMETR3:12
for R being ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) st R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) is bounded_below holds
ex s being ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) st
( s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is non-increasing & s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) is convergent & rng s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V168() V169() V170() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) c= R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) & lim s : ( ( Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) -valued Function-like V33( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) V158() V159() V160() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) = lower_bound R : ( ( non empty ) ( non empty V168() V169() V170() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) ) ;

theorem :: TOPMETR3:13
for X being ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) -defined the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( V168() V169() V170() ) set ) , ( ( ) ( non empty ) set ) )
for F1, F2 being ( ( ) ( ) Subset of )
for r1, r2 being ( ( ) ( V11() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V120() V121() V168() V169() V170() V171() V172() V173() V174() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) <= r1 : ( ( ) ( V11() real ext-real ) Real) & r2 : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) & r1 : ( ( ) ( V11() real ext-real ) Real) <= r2 : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) -defined the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( V168() V169() V170() ) set ) , ( ( ) ( non empty ) set ) ) . r1 : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) in F1 : ( ( ) ( ) Subset of ) & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) -defined the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( V168() V169() V170() ) set ) , ( ( ) ( non empty ) set ) ) . r2 : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) in F2 : ( ( ) ( ) Subset of ) & F1 : ( ( ) ( ) Subset of ) is closed & F2 : ( ( ) ( ) Subset of ) is closed & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) -defined the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( V168() V169() V170() ) set ) , ( ( ) ( non empty ) set ) ) is continuous & F1 : ( ( ) ( ) Subset of ) \/ F2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = the carrier of X : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) holds
ex r being ( ( ) ( V11() real ext-real ) Real) st
( r1 : ( ( ) ( V11() real ext-real ) Real) <= r : ( ( ) ( V11() real ext-real ) Real) & r : ( ( ) ( V11() real ext-real ) Real) <= r2 : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) -defined the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( TopSpace-like V116() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V116() ) TopStruct ) ) : ( ( ) ( V168() V169() V170() ) set ) , the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( V168() V169() V170() ) set ) , ( ( ) ( non empty ) set ) ) . r : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) in F1 : ( ( ) ( ) Subset of ) /\ F2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TOPMETR3:14
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) )
for p1, p2 being ( ( ) ( V43(b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Point of ( ( ) ( non empty ) set ) )
for P, P1 being ( ( non empty ) ( non empty ) Subset of ) st P : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of p1 : ( ( ) ( V43(b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V43(b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Point of ( ( ) ( non empty ) set ) ) & P1 : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of p2 : ( ( ) ( V43(b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Point of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( V43(b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Point of ( ( ) ( non empty ) set ) ) & P1 : ( ( non empty ) ( non empty ) Subset of ) c= P : ( ( non empty ) ( non empty ) Subset of ) holds
P1 : ( ( non empty ) ( non empty ) Subset of ) = P : ( ( non empty ) ( non empty ) Subset of ) ;

theorem :: TOPMETR3:15
for P, P1 being ( ( non empty compact ) ( non empty compact ) Subset of ) st P : ( ( non empty compact ) ( non empty compact ) Subset of ) is being_simple_closed_curve & P1 : ( ( non empty compact ) ( non empty compact ) Subset of ) is_an_arc_of W-min P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V192() ) ( non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() ) L15()) : ( ( ) ( non empty ) set ) ) , E-max P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) V117() V160() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V192() ) ( non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() ) L15()) : ( ( ) ( non empty ) set ) ) & P1 : ( ( non empty compact ) ( non empty compact ) Subset of ) c= P : ( ( non empty compact ) ( non empty compact ) Subset of ) & not P1 : ( ( non empty compact ) ( non empty compact ) Subset of ) = Upper_Arc P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V192() ) ( non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
P1 : ( ( non empty compact ) ( non empty compact ) Subset of ) = Lower_Arc P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() ) Element of K6(REAL : ( ( ) ( non empty V36() V168() V169() V170() V174() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V192() ) ( non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;