let r, s be Real; :: thesis: ( r <= s implies ex B being Basis of () st
( ex f being ManySortedSet of () st
for y being Point of () holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of () st X in B holds
X is connected ) ) )

set L = Closed-Interval-TSpace (r,s);
set M = Closed-Interval-MSpace (r,s);
assume A1: r <= s ; :: thesis: ex B being Basis of () st
( ex f being ManySortedSet of () st
for y being Point of () holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of () st X in B holds
X is connected ) )

defpred S1[ object , object ] means ex x being Point of () ex y being Point of () ex B being Basis of st
( \$1 = x & x = y & \$2 = B & B = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } );
A2: Closed-Interval-TSpace (r,s) = TopSpaceMetr () by TOPMETR:def 7;
A3: for i being object st i in the carrier of () holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in the carrier of () implies ex j being object st S1[i,j] )
assume i in the carrier of () ; :: thesis: ex j being object st S1[i,j]
then reconsider i = i as Point of () ;
reconsider m = i as Point of () by ;
reconsider j = i as Element of () by A2;
set B = Balls j;
A4: ex y being Point of () st
( y = j & Balls j = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) by FRECHET:def 1;
reconsider B1 = Balls j as Basis of by A2;
take Balls j ; :: thesis: S1[i, Balls j]
take i ; :: thesis: ex y being Point of () ex B being Basis of st
( i = i & i = y & Balls j = B & B = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )

take m ; :: thesis: ex B being Basis of st
( i = i & i = m & Balls j = B & B = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } )

take B1 ; :: thesis: ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } )
thus ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } ) by A4; :: thesis: verum
end;
consider f being ManySortedSet of the carrier of () such that
A5: for i being object st i in the carrier of () holds
S1[i,f . i] from for x being Element of () holds f . x is Basis of
proof
let x be Element of (); :: thesis: f . x is Basis of
S1[x,f . x] by A5;
hence f . x is Basis of ; :: thesis: verum
end;
then reconsider B = Union f as Basis of () by TOPGEN_2:2;
take B ; :: thesis: ( ex f being ManySortedSet of () st
for y being Point of () holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of () st X in B holds
X is connected ) )

hereby :: thesis: for X being Subset of () st X in B holds
X is connected
take f = f; :: thesis: for x being Point of () holds
( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f )

let x be Point of (); :: thesis: ( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f )
the carrier of () = [.r,s.] by
.= the carrier of () by ;
then S1[x,f . x] by A5;
hence ( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) ; :: thesis: verum
end;
let X be Subset of (); :: thesis: ( X in B implies X is connected )
assume X in B ; :: thesis: X is connected
then X in union (rng f) by CARD_3:def 4;
then consider Z being set such that
A6: X in Z and
A7: Z in rng f by TARSKI:def 4;
consider x being object such that
A8: x in dom f and
A9: f . x = Z by ;
consider x1 being Point of (), y being Point of (), B1 being Basis of such that
x = x1 and
x1 = y and
A10: ( f . x = B1 & B1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) by A5, A8;
consider n being Nat such that
A11: X = Ball (y,(1 / n)) and
n <> 0 by A6, A9, A10;
reconsider X1 = X as Subset of R^1 by PRE_TOPC:11;
( Ball (y,(1 / n)) = [.r,s.] or Ball (y,(1 / n)) = [.r,(y + (1 / n)).[ or Ball (y,(1 / n)) = ].(y - (1 / n)),s.] or Ball (y,(1 / n)) = ].(y - (1 / n)),(y + (1 / n)).[ ) by ;
then X1 is connected by A11;
hence X is connected by CONNSP_1:23; :: thesis: verum