reconsider D = DiscreteSpace 2 as non empty MetrSpace ;
reconsider a = 0 , b = 1 as Point of D by NAT_1:44;
TopSpaceMetr D is compact by COMPTS_1:18;
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 bounded SetSequence of (WellSpace (a,NAT)) st
( S is closed & S is non-ascending & meet S is empty ) by A1, Th43;
WellSpace (a,NAT) is complete by A2, A1, Th43;
hence ex M being non empty MetrSpace st
( M is complete & ex S being non-empty bounded SetSequence of M st
( S is closed & S is non-ascending & meet S is empty ) ) by A3; :: thesis: verum