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

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