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 V176() & meet S is empty ) )