consider x being set such that
A1: x in the carrier of M by XBOOLE_0:def 1;
reconsider x = x as Point of M by A1;
reconsider X = {x} as Subset of M ;

A2: now

let x1, x2 be Point of M; :: thesis: ( x1 in X & x2 in X implies dist x1,x2 <= 1 )
assume A3: ( x1 in X & x2 in X ) ; :: thesis: dist x1,x2 <= 1
( x1 = x & x2 = x ) by A3, TARSKI:def 1;
hence dist x1,x2 <= 1 by METRIC_1:1; :: thesis: verum

end;

take S = NAT --> X; :: thesis: ( S is bounded & S is non-empty )

A5: now

let i be natural number ; :: thesis: S . i is bounded
reconsider i' = i as Element of NAT by ORDINAL1:def 13;
( X is bounded & S . i' = X ) by A2, FUNCOP_1:13, TBSP_1:def 9;
hence S . i is bounded ; :: thesis: verum

end;

for x being set st x in dom S holds
not S . x is empty by FUNCOP_1:13;
hence ( S is bounded & S is non-empty ) by A5, Def1, FUNCT_1:def 15; :: thesis: verum