let r, s be real number ; :: 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 Element of 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 Element of 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₁[ 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 st
( $1 = x & x = y & $2 = B & B = { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } );
A2: Closed-Interval-TSpace r,s = TopSpaceMetr (Closed-Interval-MSpace r,s) by TOPMETR:def 8;
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]

proof

let i be set ; :: thesis: ( i in the carrier of (Closed-Interval-TSpace r,s) implies ex j being set st S₁[i,j] )
assume i in the carrier of (Closed-Interval-TSpace r,s) ; :: thesis: ex j being set 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:16;
reconsider j = i as Element of (TopSpaceMetr (Closed-Interval-MSpace r,s)) by A2, TOPMETR:16;
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 Element of NAT : n <> 0 } ) by FRECHET:def 1;
reconsider B1 = Balls j as Basis of by A2, TOPMETR:16;
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 Element of 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 Element of NAT : n <> 0 } )
take B1 ; :: thesis: ( i = i & i = m & Balls j = B1 & B1 = { (Ball m,(1 / n)) where n is Element of NAT : n <> 0 } )
thus ( i = i & i = m & Balls j = B1 & B1 = { (Ball m,(1 / n)) where n is Element of 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 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

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 Element of 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 Element of 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 Element of NAT : n <> 0 } & B = Union f )
the carrier of (Closed-Interval-MSpace r,s) = [.r,s.] by A1, TOPMETR:14
.= the carrier of (Closed-Interval-TSpace r,s) by A1, 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: 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 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 such that
x = x1 and
x1 = y and
A10: ( 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
n <> 0 by A6, A9, A10;
reconsider X1 = X as Subset of R^1 by PRE_TOPC:39;
( 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, RCOMP_3:52;
hence X is connected by CONNSP_1:24; :: thesis: verum