let r, s be real number ; :: 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 st
for y being Point of (Closed-Interval-MSpace r,s) holds
( f . y = { (Ball y,(1 / n)) where n is Element of 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