theorem Th9: :: COMPL_SP:9

for M being non empty MetrSpace
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 pointwise_bounded & lim (diameter S) = 0 ) ) & ( for i being Nat ex U being Subset of (TopSpaceMetr M) st
( U = { (C . j) where j is Nat : j >= i } & S . i = Cl U ) ) )