theorem Th2: :: COMPL_SP:2

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