theorem Th2: :: TOPALG_5:2

for r, s being Real st r <= s holds
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 ) )