for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M holds diameter S is bounded_below