theorem :: COMPL_SP:3

for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is non-descending holds
diameter S is non-decreasing