for M being non empty Reflexive symmetric triangle MetrStruct st M is complete holds
for a being Point of M st ex b being Point of M st dist (a,b) <> 0 holds
for X being infinite set holds
( WellSpace (a,X) is complete & ex S being non-empty pointwise_bounded SetSequence of (WellSpace (a,X)) st
( S is closed & S is V176() & meet S is empty ) )