let M be non empty Reflexive symmetric triangle MetrSpace; :: thesis:
set T = TopSpaceMetr M;
let C be sequence of M; :: thesis:
defpred S₁[ set , set ] means for i being natural number st i = $1 holds
ex S being Subset of (TopSpaceMetr M) st
( S = { (C . j) where j is Element of NAT : j >= i } & $2 = Cl S );
A1: for x being set st x in NAT holds
ex y being set st
( y in bool the carrier of M & S₁[x,y] )

let x be set ; :: thesis:
assume A2: x in NAT ; :: thesis:
reconsider x' = x as Element of NAT by A2;
set S = { (C . j) where j is Element of NAT : j >= x' } ;
{ (C . j) where j is Element of NAT : j >= x' } c= the carrier of (TopSpaceMetr M)

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A3: y in { (C . j) where j is Element of NAT : j >= x' } ; :: thesis:
ex j being Element of NAT st
( C . j = y & j >= x' ) by A3;
hence y in the carrier of (TopSpaceMetr M) ; :: thesis:

end;

then reconsider S = { (C . j) where j is Element of NAT : j >= x' } as Subset of (TopSpaceMetr M) ;
take CL = Cl S; :: thesis:
thus ( CL in bool the carrier of M & S₁[x,CL] ) ; :: thesis:

end;

consider S being SetSequence of M such that
A4: for x being set st x in NAT holds
S₁[x,S . x] from FUNCT_2:sch 1(A1);

A5: now

let x be set ; :: thesis:
assume A6: x in dom S ; :: thesis:
reconsider i = x as Element of NAT by A6;
consider U being Subset of (TopSpaceMetr M) such that
A7: ( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by A4;
( C . i in U & U c= S . i ) by A7, PRE_TOPC:48;
hence not S . x is empty ; :: thesis:

end;

now

let i be natural number ; :: thesis:
i in NAT by ORDINAL1:def 13;
then ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by A4;
hence S . i is closed by Th6; :: thesis:

end;

then reconsider S = S as non-empty closed SetSequence of M by A5, Def8, FUNCT_1:def 15;
take S ; :: thesis:

let i be Element of NAT ; :: thesis:
consider U being Subset of (TopSpaceMetr M) such that
A8: ( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by A4;
consider U1 being Subset of (TopSpaceMetr M) such that
A9: ( U1 = { (C . j) where j is Element of NAT : j >= i + 1 } & S . (i + 1) = Cl U1 ) by A4;
U1 c= U

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in U1 ; :: thesis:
consider j being Element of NAT such that
A11: ( x = C . j & j >= i + 1 ) by A9, A10;
j >= i by A11, NAT_1:13;
hence x in U by A8, A11; :: thesis:

end;

hence S . (i + 1) c= S . i by A8, A9, PRE_TOPC:49; :: thesis:

end;

hence A12: S is non-ascending by KURATO_2:def 5; :: thesis:
thus ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) :: thesis:

assume A13: C is Cauchy ; :: thesis:

A14: now

let i be natural number ; :: thesis:
i in NAT by ORDINAL1:def 13;
then consider U being Subset of (TopSpaceMetr M) such that
A15: ( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by A4;
reconsider U' = U as Subset of M ;
U c= rng C

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A16: x in U ; :: thesis:
( dom C = NAT & ex j being Element of NAT st
( x = C . j & j >= i ) ) by A15, A16, FUNCT_2:def 1;
hence x in rng C by FUNCT_1:def 5; :: thesis:

end;

then U' is bounded by A13, TBSP_1:21, TBSP_1:34;
hence S . i is bounded by A15, Th8; :: thesis:

end;

hence S is bounded by Def1; :: thesis:
reconsider S' = S as non-empty bounded closed SetSequence of M by A14, Def1;
set d = diameter S';
B17: ( diameter S' is bounded_below & diameter S' is non-increasing ) by A12, Th1, Th2;
for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((diameter S') . m) - 0 ) < r

let r be real number ; :: thesis:
assume A18: 0 < r ; :: thesis:
reconsider R = r as Real by XREAL_0:def 1;
set R2 = R / 2;
R / 2 > 0 by A18, XREAL_1:141;
then consider p being Element of NAT such that
A19: for n, m being Element of NAT st p <= n & p <= m holds
dist (C . n),(C . m) < R / 2 by A13, TBSP_1:def 5;
take p ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A20: p <= m ; :: thesis:
consider U being Subset of (TopSpaceMetr M) such that
A21: ( U = { (C . j) where j is Element of NAT : j >= m } & S . m = Cl U ) by A4;
reconsider U' = U as Subset of M ;
A22: U c= rng C

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: x in U ; :: thesis:
( dom C = NAT & ex j being Element of NAT st
( x = C . j & j >= m ) ) by A21, A23, FUNCT_2:def 1;
hence x in rng C by FUNCT_1:def 5; :: thesis:

end;

A24: ( rng C is bounded & C . m in U ) by A13, A21, TBSP_1:34;
then A25: ( U' is bounded & not U' is empty ) by A22, TBSP_1:21;

let x, y be Point of M; :: thesis:
assume A26: ( x in U' & y in U' ) ; :: thesis:
consider i being Element of NAT such that
A27: ( x = C . i & i >= m ) by A21, A26;
consider j being Element of NAT such that
A28: ( y = C . j & j >= m ) by A21, A26;
( i >= p & j >= p ) by A20, A27, A28, XXREAL_0:2;
hence dist x,y <= R / 2 by A19, A27, A28; :: thesis:

end;

then ( diameter U' <= R / 2 & diameter U' = diameter (S . m) ) by A21, A25, Th8, TBSP_1:def 10;
then ( diameter (S . m) <= R / 2 & diameter (S . m) >= 0 ) by A22, A24, TBSP_1:21, TBSP_1:29;
then ( abs (diameter (S . m)) <= R / 2 & R / 2 < R ) by A18, ABSVALUE:def 1, XREAL_1:218;
then ( abs (diameter (S . m)) < R & diameter (S . m) = (diameter S') . m ) by Def2, XXREAL_0:2;
hence abs (((diameter S') . m) - 0 ) < r ; :: thesis:

end;

hence lim (diameter S) = 0 by B17, SEQ_2:def 7; :: thesis:

end;

let i be natural number ; :: thesis:
i in NAT by ORDINAL1:def 13;
hence ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by A4; :: thesis: