let Z be non empty MetrSpace; :: thesis: for F being non empty Subset of Z st Z is complete holds
Z | (Cl F) is complete
let F be non empty Subset of Z; :: thesis: ( Z is complete implies Z | (Cl F) is complete )
assume A1: Z is complete ; :: thesis: Z | (Cl F) is complete
set N = Z | (Cl F);
A2: the carrier of (Z | (Cl F)) = Cl F by TOPMETR:def 2;
let S2 be sequence of (Z | (Cl F)); :: according to TBSP_1:def 5 :: thesis: ( not S2 is Cauchy or S2 is convergent )
assume A3: S2 is Cauchy ; :: thesis: S2 is convergent
A4: rng S2 c= Cl F by A2;
rng S2 c= the carrier of Z by A2, XBOOLE_1:1;
then reconsider S1 = S2 as sequence of Z by FUNCT_2:6;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((S1 . n),(S1 . m)) < r

proof

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((S1 . n),(S1 . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((S1 . n),(S1 . m)) < r
then consider p being Nat such that
A6: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A3;
take p ; :: thesis: for n, m being Nat st n >= p & m >= p holds
dist ((S1 . n),(S1 . m)) < r
let n, m be Nat; :: thesis: ( n >= p & m >= p implies dist ((S1 . n),(S1 . m)) < r )
assume ( p <= n & p <= m ) ; :: thesis: dist ((S1 . n),(S1 . m)) < r
then dist ((S2 . n),(S2 . m)) < r by A6;
hence dist ((S1 . n),(S1 . m)) < r by TOPMETR:def 1; :: thesis: verum

end;

then a7: S1 is Cauchy ;
then A8: S1 is_convergent_in_metrspace_to lim S1 by A1, METRIC_6:12;
consider H being Subset of (TopSpaceMetr Z) such that
A9: ( H = F & Cl F = Cl H ) by ASCOLI:def 1;
for n being Nat holds S1 . n in Cl H

proof

let n be Nat; :: thesis: S1 . n in Cl H
S1 . n in rng S1 by FUNCT_2:4, ORDINAL1:def 12;
hence S1 . n in Cl H by A4, A9; :: thesis: verum

end;

then lim S1 in Cl F by TOPMETR4:6, A9, a7, A1;
then reconsider L = lim S1 as Point of (Z | (Cl F)) by TOPMETR:def 2;
reconsider L0 = L as Point of Z ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r
then consider m being Nat such that
A10: for n being Nat st m <= n holds
dist ((S1 . n),L0) < r by METRIC_6:def 2, A8;
take m ; :: thesis: for n being Nat st m <= n holds
dist ((S2 . n),L) < r
let n be Nat; :: thesis: ( m <= n implies dist ((S2 . n),L) < r )
assume m <= n ; :: thesis: dist ((S2 . n),L) < r
then dist ((S1 . n),L0) < r by A10;
hence dist ((S2 . n),L) < r by TOPMETR:def 1; :: thesis: verum

end;

hence S2 is convergent ; :: thesis: verum