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

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Nat ;
set S = { (C . j) where j is Nat : j >= x9 } ;
{ (C . j) where j is Nat : j >= x9 } c= the carrier of (TopSpaceMetr M)

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

end;

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

end;

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

let x be object ; :: thesis:
assume x in dom S ; :: thesis:
then reconsider i = x as Element of NAT ;
consider U being Subset of (TopSpaceMetr M) such that
A4: U = { (C . j) where j is 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:

end;

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

end;

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

let i be Nat; :: thesis:
i in NAT by ORDINAL1:def 12;
then consider U being Subset of (TopSpaceMetr M) such that
A7: U = { (C . j) where j is 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 Nat : j >= i + 1 } and
A10: S . (i + 1) = Cl U1 by A2;
U1 c= U

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in U1 ; :: thesis:
then consider j being 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:

end;

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in U ; :: thesis:
then consider j being Nat such that
A18: ( x = C . j & j >= i ) by A16;
A19: j in NAT by ORDINAL1:def 12;
dom C = NAT by FUNCT_2:def 1;
hence x in rng C by A18, FUNCT_1:def 3, A19; :: thesis:

end;

end;

then reconsider S9 = S as non-empty pointwise_bounded closed SetSequence of M by Def1;
set d = diameter S9;
A20: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((diameter S9) . m) - 0).| < r

let r be Real; :: thesis:
assume A21: 0 < r ; :: thesis:
reconsider R = r as Real ;
set R2 = R / 2;
R / 2 > 0 by A21, XREAL_1:139;
then consider p being Nat such that
A22: for n, m being Nat st p <= n & p <= m holds
dist ((C . n),(C . m)) < R / 2 by A14;
take p ; :: thesis:
let m be Nat; :: thesis:
assume A23: p <= m ; :: thesis:
m in NAT by ORDINAL1:def 12;
then consider U being Subset of (TopSpaceMetr M) such that
A24: U = { (C . j) where j is Nat : j >= m } and
A25: S . m = Cl U by A2;
reconsider U9 = U as Subset of M ;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in U ; :: thesis:
then consider j being Nat such that
A35: ( x = C . j & j >= m ) by A24;
A36: j in NAT by ORDINAL1:def 12;
dom C = NAT by FUNCT_2:def 1;
hence x in rng C by A35, FUNCT_1:def 3, A36; :: thesis:

end;

end;

end;

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