let r, s be real number ; :: thesis:
set L = Closed-Interval-TSpace r,s;
set M = Closed-Interval-MSpace r,s;
A1: Closed-Interval-TSpace r,s = TopSpaceMetr (Closed-Interval-MSpace r,s) by TOPMETR:def 8;
assume A2: r <= s ; :: thesis:
defpred S₁[ set , set ] 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 x st
( $1 = x & x = y & $2 = B & B = { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } );
A3: for i being set st i in the carrier of (Closed-Interval-TSpace r,s) holds
ex j being set st S₁[i,j]

let i be set ; :: thesis:
assume i in the carrier of (Closed-Interval-TSpace r,s) ; :: thesis:
then reconsider i = i as Point of (Closed-Interval-TSpace r,s) ;
reconsider m = i as Point of (Closed-Interval-MSpace r,s) by A1, TOPMETR:16;
consider B being Basis of i such that
A4: B = { (Ball m,(1 / n)) where n is Element of NAT : n <> 0 } and
( B is countable & ex f being Function of NAT ,B st
for n being set st n in NAT holds
ex n' being Element of NAT st
( n = n' & f . n = Ball m,(1 / (n' + 1)) ) ) by A1, FRECHET:11;
take B ; :: thesis:
take i ; :: thesis:
take m ; :: thesis:
take B ; :: thesis:
thus ( i = i & i = m & B = B & B = { (Ball m,(1 / n)) where n is Element of NAT : n <> 0 } ) by A4; :: thesis:

end;

consider f being ManySortedSet of such that
A5: for i being set 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 x

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

end;

then reconsider B = Union f as Basis of Closed-Interval-TSpace r,s by TOPGEN_2:2;
take B ; :: thesis:

hereby :: thesis:

take f = f; :: thesis:
let x be Point of (Closed-Interval-MSpace r,s); :: thesis:
the carrier of (Closed-Interval-MSpace r,s) = [.r,s.] by A2, TOPMETR:14
.= the carrier of (Closed-Interval-TSpace r,s) by A2, TOPMETR:25 ;
then S₁[x,f . x] by A5;
hence ( f . x = { (Ball x,(1 / n)) where n is Element of NAT : n <> 0 } & B = Union f ) ; :: thesis:

end;

let X be Subset of (Closed-Interval-TSpace r,s); :: thesis:
assume X in B ; :: thesis:
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 set such that
A8: x in dom f and
A9: f . x = Z by A7, FUNCT_1:def 5;
dom f = the carrier of (Closed-Interval-TSpace r,s) by PARTFUN1:def 4;
then consider x1 being Point of (Closed-Interval-TSpace r,s), y being Point of (Closed-Interval-MSpace r,s), B1 being Basis of x1 such that
A10: ( x = x1 & x1 = y & f . x = B1 & B1 = { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } ) by A5, A8;
consider n being Element of NAT such that
A11: X = Ball y,(1 / n) and
A12: n <> 0 by A6, A9, A10;
reconsider X1 = X as Subset of R^1 by PRE_TOPC:39;
0 < n by A12;
then 1 / n > 0 by XREAL_1:141;
then ( 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 A2, Th1;
then X1 is connected by A11, RCOMP_3:52;
hence X is connected by CONNSP_1:24; :: thesis: