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_{1}[ 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_{1}[i,j]

A5: for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds

S_{1}[i,f . i]
from PBOOLE:sch 3(A3);

for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of

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 ) )

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

( 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

( $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

proof

consider f being ManySortedSet of the carrier of (Closed-Interval-TSpace (r,s)) such that
let i be object ; :: thesis: ( i in the carrier of (Closed-Interval-TSpace (r,s)) implies ex j being object st S_{1}[i,j] )

assume i in the carrier of (Closed-Interval-TSpace (r,s)) ; :: thesis: ex j being object st S_{1}[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_{1}[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;assume i in the carrier of (Closed-Interval-TSpace (r,s)) ; :: thesis: ex j being object st S

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

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

A5: for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds

S

for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of

proof

then reconsider B = Union f as Basis of (Closed-Interval-TSpace (r,s)) by TOPGEN_2:2;
let x be Element of (Closed-Interval-TSpace (r,s)); :: thesis: f . x is Basis of

S_{1}[x,f . x]
by A5;

hence f . x is Basis of ; :: thesis: verum

end;S

hence f . x is Basis of ; :: thesis: verum

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

let X be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: ( X in B implies X is connected )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_{1}[x,f . x]
by A5;

hence ( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) ; :: thesis: verum

end;( 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

hence ( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) ; :: thesis: verum

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