reconsider D = DiscreteSpace 2 as non empty MetrSpace ;
( 0 in Segm 2 & 1 in Segm 2 ) by NAT_1:44;
then reconsider a = 0 , b = 1 as Point of D ;
TopSpaceMetr D is compact ;
then A1: D is complete by TBSP_1:8;
A2: 1 = dist (a,b) by METRIC_1:def 10;
then A3: ex S being non-empty pointwise_bounded SetSequence of (WellSpace (a,NAT)) st
( S is closed & S is V176() & meet S is empty ) by A1, Th42;
WellSpace (a,NAT) is complete by A2, A1, Th42;
hence 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 ) ) by A3; :: thesis: verum