for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V176() & lim (diameter S) = 0 holds
for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy