let r, s be Real; :: thesis: ( r <= s implies 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 ) ) )
set L = Closed-Interval-TSpace (r,s);
set M = Closed-Interval-MSpace (r,s);
assume A1: r <= s ; :: thesis: 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 ) )
defpred S₁[ object , object ] means ex x being Point of (Closed-Interval-TSpace (r,s)) ex y being Point of (Closed-Interval-MSpace (r,s)) 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 (Closed-Interval-MSpace (r,s)) by TOPMETR:def 7;
A3: for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in the carrier of (Closed-Interval-TSpace (r,s)) implies ex j being object st S₁[i,j] )
assume i in the carrier of (Closed-Interval-TSpace (r,s)) ; :: thesis: ex j being object st S₁[i,j]
then reconsider i = i as Point of (Closed-Interval-TSpace (r,s)) ;
reconsider m = i as Point of (Closed-Interval-MSpace (r,s)) by A2, TOPMETR:12;
reconsider j = i as Element of (TopSpaceMetr (Closed-Interval-MSpace (r,s))) by A2;
set B = Balls j;
A4: ex y being Point of (Closed-Interval-MSpace (r,s)) 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: S₁[i, Balls j]
take i ; :: thesis: ex y being Point of (Closed-Interval-MSpace (r,s)) 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 (Closed-Interval-TSpace (r,s)) such that
A5: for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
S₁[i,f . i] from PBOOLE:sch 3(A3);
for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of

proof

let x be Element of (Closed-Interval-TSpace (r,s)); :: thesis: f . x is Basis of
S₁[x,f . x] by A5;
hence f . x is Basis of ; :: thesis: verum

end;

then reconsider B = Union f as Basis of (Closed-Interval-TSpace (r,s)) by TOPGEN_2:2;
take B ; :: thesis: ( 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 ) )

hereby :: thesis: for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected

take f = f; :: thesis: for x being Point of (Closed-Interval-MSpace (r,s)) holds
( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f )
let x be Point of (Closed-Interval-MSpace (r,s)); :: thesis: ( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f )
the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.] by A1, TOPMETR:10
.= the carrier of (Closed-Interval-TSpace (r,s)) by A1, TOPMETR:18 ;
then S₁[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 (Closed-Interval-TSpace (r,s)); :: 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 A7, FUNCT_1:def 3;
consider x1 being Point of (Closed-Interval-TSpace (r,s)), y being Point of (Closed-Interval-MSpace (r,s)), 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 A1, Th1;
then X1 is connected by A11;
hence X is connected by CONNSP_1:23; :: thesis: verum