let M be non empty MetrSpace; :: thesis: for C being sequence of M ex S being non-empty closed SetSequence of M st
( S is non-ascending & ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) & ( for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) ) )
set T = TopSpaceMetr M;
let C be sequence of M; :: thesis: ex S being non-empty closed SetSequence of M st
( S is non-ascending & ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) & ( for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) ) )
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] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool the carrier of M & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in bool the carrier of M & S₁[x,y] )
then reconsider x9 = x as Element of NAT ;
set S = { (C . j) where j is Element of NAT : j >= x9 } ;
{ (C . j) where j is Element of NAT : j >= x9 } c= the carrier of (TopSpaceMetr M)

proof

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

end;

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

end;

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

A3: now

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

end;

now

let i be natural number ; :: thesis: S . i is closed
i in NAT by ORDINAL1:def 12;
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 A2;
hence S . i is closed by Th6; :: thesis: verum

end;

then reconsider S = S as non-empty closed SetSequence of M by A3, Def8, FUNCT_1:def 9;
take S ; :: thesis: ( S is non-ascending & ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) & ( for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) ) )

now

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

proof

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

end;

hence S . (i + 1) c= S . i by A8, A10, PRE_TOPC:19; :: thesis: verum

end;

hence A13: S is non-ascending by KURATO_0:def 3; :: thesis: ( ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) & ( for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U ) ) )
thus ( C is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) :: thesis: for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U )

proof

assume A14: C is Cauchy ; :: thesis: ( S is bounded & lim (diameter S) = 0 )

A15: now

let i be natural number ; :: thesis: S . i is bounded
i in NAT by ORDINAL1:def 12;
then consider U being Subset of (TopSpaceMetr M) such that
A16: U = { (C . j) where j is Element of NAT : j >= i } and
A17: S . i = Cl U by A2;
reconsider U9 = U as Subset of M ;
U c= rng C

proof

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

end;

then U9 is bounded by A14, TBSP_1:14, TBSP_1:26;
hence S . i is bounded by A17, Th8; :: thesis: verum

end;

then reconsider S9 = S as non-empty bounded closed SetSequence of M by Def1;
set d = diameter S9;
A19: 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 S9) . m) - 0) < r

proof

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((diameter S9) . m) - 0) < r )
assume A20: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((diameter S9) . m) - 0) < r
reconsider R = r as Real by XREAL_0:def 1;
set R2 = R / 2;
R / 2 > 0 by A20, XREAL_1:139;
then consider p being Element of NAT such that
A21: for n, m being Element of NAT st p <= n & p <= m holds
dist ((C . n),(C . m)) < R / 2 by A14, TBSP_1:def 4;
take p ; :: thesis: for m being Element of NAT st p <= m holds
abs (((diameter S9) . m) - 0) < r
let m be Element of NAT ; :: thesis: ( p <= m implies abs (((diameter S9) . m) - 0) < r )
assume A22: p <= m ; :: thesis: abs (((diameter S9) . m) - 0) < r
consider U being Subset of (TopSpaceMetr M) such that
A23: U = { (C . j) where j is Element of NAT : j >= m } and
A24: S . m = Cl U by A2;
reconsider U9 = U as Subset of M ;

A25: now

let x, y be Point of M; :: thesis: ( x in U9 & y in U9 implies dist (x,y) <= R / 2 )
assume that
A26: x in U9 and
A27: y in U9 ; :: thesis: dist (x,y) <= R / 2
consider j being Element of NAT such that
A28: y = C . j and
A29: j >= m by A23, A27;
A30: j >= p by A22, A29, XXREAL_0:2;
consider i being Element of NAT such that
A31: x = C . i and
A32: i >= m by A23, A26;
i >= p by A22, A32, XXREAL_0:2;
hence dist (x,y) <= R / 2 by A21, A31, A28, A30; :: thesis: verum

end;

A33: U c= rng C

proof

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

end;

then A35: U9 is bounded by A14, TBSP_1:14, TBSP_1:26;
then A36: diameter U9 = diameter (S . m) by A24, Th8;
C . m in U by A23;
then A37: diameter U9 <= R / 2 by A35, A25, TBSP_1:def 8;
rng C is bounded by A14, TBSP_1:26;
then diameter (S . m) >= 0 by A33, A36, TBSP_1:14, TBSP_1:21;
then A38: abs (diameter (S . m)) <= R / 2 by A37, A36, ABSVALUE:def 1;
R / 2 < R by A20, XREAL_1:216;
then abs (diameter (S . m)) < R by A38, XXREAL_0:2;
hence abs (((diameter S9) . m) - 0) < r by Def2; :: thesis: verum

end;

thus S is bounded by A15, Def1; :: thesis: lim (diameter S) = 0
A39: diameter S9 is bounded_below by Th1;
diameter S9 is non-increasing by A13, Th2;
hence lim (diameter S) = 0 by A39, A19, SEQ_2:def 7; :: thesis: verum

end;

let i be natural number ; :: thesis: ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Element of NAT : j >= i } & S . i = Cl U )
i in NAT by ORDINAL1:def 12;
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 A2; :: thesis: verum