for r, s, a being ( ( real ) ( V11() ext-real real ) number ) st r : ( ( real ) ( V11() ext-real real ) number ) <= s : ( ( real ) ( V11() ext-real real ) number ) holds
for p being ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) holds
( Ball (p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V213() V214() V215() ) Element of bool the carrier of (Closed-Interval-MSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) MetrStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) : ( ( ) ( non empty ) set ) ) = [.r : ( ( real ) ( V11() ext-real real ) number ) ,s : ( ( real ) ( V11() ext-real real ) number ) .] : ( ( ) ( V213() V214() V215() V320() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) or Ball (p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V213() V214() V215() ) Element of bool the carrier of (Closed-Interval-MSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) MetrStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) : ( ( ) ( non empty ) set ) ) = [.r : ( ( real ) ( V11() ext-real real ) number ) ,(p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) + a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) .[ : ( ( ) ( V213() V214() V215() V316() V317() V318() V319() V320() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) or Ball (p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V213() V214() V215() ) Element of bool the carrier of (Closed-Interval-MSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) MetrStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) : ( ( ) ( non empty ) set ) ) = ].(p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) - a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ,s : ( ( real ) ( V11() ext-real real ) number ) .] : ( ( ) ( V213() V214() V215() V315() V317() V318() V319() V320() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) or Ball (p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V213() V214() V215() ) Element of bool the carrier of (Closed-Interval-MSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) MetrStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) : ( ( ) ( non empty ) set ) ) = ].(p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) - a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ,(p : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) + a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) .[ : ( ( ) ( V213() V214() V215() V315() V316() V317() V318() V319() V320() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

for r, s being ( ( real ) ( V11() ext-real real ) number ) st r : ( ( real ) ( V11() ext-real real ) number ) <= s : ( ( real ) ( V11() ext-real real ) number ) holds
ex B being ( ( quasi_basis open ) ( quasi_basis open ) Basis of Closed-Interval-TSpace (r : ( ( real ) ( V11() ext-real real ) number ) ,s : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ) st
( ex f being ( ( Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined Function-like V26( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) ) ( Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined Function-like V26( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) ) ManySortedSet of ( ( ) ( non empty V213() V214() V215() ) set ) ) st
for y being ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) holds
( f : ( ( ) ( V213() V214() V215() ) Subset of ) . y : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) : ( ( ) ( ) set ) = { (Ball (y : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,(1 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real integer V34() V213() V214() V215() V216() V217() V218() V315() V317() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) / n : ( ( ) ( ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() ext-real non negative real ) Element of REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) ) )) : ( ( ) ( V213() V214() V215() ) Element of bool the carrier of (Closed-Interval-MSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V302() ) MetrStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) : ( ( ) ( non empty ) set ) ) where n is ( ( ) ( ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) : n : ( ( ) ( ordinal natural V11() ext-real non negative real integer V34() V213() V214() V215() V216() V217() V218() V317() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) <> 0 : ( ( ) ( empty ordinal natural V11() ext-real non positive non negative real Function-like functional integer V34() FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) } & B : ( ( quasi_basis open ) ( quasi_basis open ) Basis of Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ) = Union f : ( ( ) ( V213() V214() V215() ) Subset of ) : ( ( ) ( ) set ) ) & ( for X being ( ( ) ( V213() V214() V215() ) Subset of ) st X : ( ( ) ( V213() V214() V215() ) Subset of ) in B : ( ( quasi_basis open ) ( quasi_basis open ) Basis of Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() ext-real real ) number ) ,b₂ : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ) holds
X : ( ( ) ( V213() V214() V215() ) Subset of ) is connected ) ) ;

for T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) Subset of )
for t being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st t : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in A : ( ( ) ( ) Subset of ) holds
Component_of (t : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ) ;

let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let A be ( ( open ) ( open ) Subset of ) ;

for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for S being ( ( ) ( TopSpace-like ) SubSpace of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) holds
T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | A : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) = S : ( ( ) ( TopSpace-like ) SubSpace of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) | B : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b₂ : ( ( ) ( TopSpace-like ) SubSpace of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ) ;

for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of )
for C, D being ( ( ) ( ) Subset of ) st TopStruct(# the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & A : ( ( ) ( ) Subset of ) = C : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) = D : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) ,B : ( ( ) ( ) Subset of ) are_separated holds
C : ( ( ) ( ) Subset of ) ,D : ( ( ) ( ) Subset of ) are_separated ;

for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st TopStruct(# the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is connected holds
T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is connected ;

for S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st TopStruct(# the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is connected holds
B : ( ( ) ( ) Subset of ) is connected ;

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) a_neighborhood of s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) a_neighborhood of b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is ( ( ) ( ) a_neighborhood of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of )
for N being ( ( ) ( ) a_neighborhood of A : ( ( ) ( ) Subset of ) ) st TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) holds
N : ( ( ) ( ) a_neighborhood of b₃ : ( ( ) ( ) Subset of ) ) is ( ( ) ( ) a_neighborhood of B : ( ( ) ( ) Subset of ) ) ;

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & A : ( ( ) ( ) Subset of ) is_a_component_of B : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is_a_component_of f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for A being ( ( non empty ) ( non empty ) Subset of )
for B being ( ( non empty ) ( non empty ) Subset of ) st A : ( ( non empty ) ( non empty ) Subset of ) = B : ( ( non empty ) ( non empty ) Subset of ) & A : ( ( non empty ) ( non empty ) Subset of ) is locally_connected holds
B : ( ( non empty ) ( non empty ) Subset of ) is locally_connected ;

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected iff [#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is locally_connected ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( non empty open ) ( non empty TopSpace-like open ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected holds
S : ( ( non empty open ) ( non empty TopSpace-like open ) SubSpace of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is locally_connected ;

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) are_homeomorphic & S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st ex B being ( ( quasi_basis open ) ( quasi_basis open ) Basis of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) in B : ( ( quasi_basis open ) ( quasi_basis open ) Basis of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
X : ( ( ) ( ) Subset of ) is connected holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally_connected ;

for r, s being ( ( real ) ( V11() ext-real real ) number ) st r : ( ( real ) ( V11() ext-real real ) number ) <= s : ( ( real ) ( V11() ext-real real ) number ) holds
Closed-Interval-TSpace (r : ( ( real ) ( V11() ext-real real ) number ) ,s : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V302() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) is locally_connected ;

let A be ( ( non empty open ) ( non empty open V213() V214() V215() ) Subset of ) ;

let r be ( ( real ) ( V11() ext-real real ) number ) ;

let r be ( ( real ) ( V11() ext-real real ) number ) ;

let r be ( ( real ) ( V11() ext-real real ) number ) ;
:: original: ExtendInt
redefine func ExtendInt r -> ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like connected V302() pathwise_connected interval first-countable Frechet sequential ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total continuous V203() V204() V205() ) Path of R^1 0 : ( ( ) ( empty ordinal natural V11() ext-real non positive non negative real Function-like functional integer V34() FinSequence-membered V213() V214() V215() V216() V217() V218() V219() V317() V320() ) Element of NAT : ( ( ) ( V213() V214() V215() V216() V217() V218() V219() V317() ) Element of bool REAL : ( ( ) ( non empty non finite V213() V214() V215() V219() V317() V318() V320() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like connected V302() pathwise_connected interval first-countable Frechet sequential ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) , R^1 r : ( ( non empty V185() V186() ) ( non empty V184() V185() V186() V235() V236() V237() V238() V239() V240() ) multMagma ) : ( ( ) ( V11() ext-real real ) Element of the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like connected V302() pathwise_connected interval first-countable Frechet sequential ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) ) ;

let S, T, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let H be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let t be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

let S, T, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let H be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let s be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

let S, T, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let H be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let t be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

let S, T, Y be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let H be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let s be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for H being ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) )
for t being ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) st H : ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of b₄ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,b₅ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) is continuous holds
Prj1 (t : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,H : ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of b₄ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,b₅ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V213() V214() V215() ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for H being ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) )
for s being ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) st H : ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of b₄ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,b₅ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) is continuous holds
Prj2 (s : ( ( ) ( V11() ext-real real ) Point of ( ( ) ( non empty V213() V214() V215() ) set ) ) ,H : ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homotopy of b₄ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,b₅ : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Path of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact locally_connected V302() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V302() first-countable Frechet sequential ) TopStruct ) ) : ( ( ) ( non empty V213() V214() V215() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V213() V214() V215() ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

let r be ( ( real ) ( V11() ext-real real ) number ) ;