reconsider D = DiscreteSpace 2 as non empty MetrSpace ;
reconsider a = 0 , b = 1 as Point of D by NAT_1:45;
TopSpaceMetr D is compact by COMPTS_1:27;
then A1: D is complete by TBSP_1:10;
A2: 1 = dist a,b by METRIC_1:def 11;
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