for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V176() holds
( diameter S is bounded_above & diameter S is non-increasing )