let r, s be Real; :: thesis: ( r <= s implies Closed-Interval-TSpace (r,s) is locally_connected )
assume r <= s ; :: thesis: Closed-Interval-TSpace (r,s) is locally_connected
then ex B being Basis of (Closed-Interval-TSpace (r,s)) st
( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st
for y being Point of (Closed-Interval-MSpace (r,s)) holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) ) by Th2;
hence Closed-Interval-TSpace (r,s) is locally_connected by Th16; :: thesis: verum