theorem :: COMPL_SP:44

ex M being non empty MetrSpace st
( M is complete & ex S being non-empty pointwise_bounded SetSequence of M st
( S is closed & S is non-ascending & meet S is empty ) )