consider x being set such that
A6: x in the carrier of M by XBOOLE_0:def 1;
reconsider x = x as Point of M by A6;
set B = cl_Ball x,1;
take S = NAT --> (cl_Ball x,1); :: thesis: ( S is non-empty & S is bounded & S is closed )

A8: now

let i be natural number ; :: thesis: S . i is bounded
( cl_Ball x,1 is bounded & i in NAT ) by ORDINAL1:def 13, TOPREAL6:67;
hence S . i is bounded by FUNCOP_1:13; :: thesis: verum

end;

A9: now

let y be set ; :: thesis: ( y in dom S implies not S . y is empty )
assume A10: y in dom S ; :: thesis: not S . y is empty
reconsider n = y as Element of NAT by A10;
dist x,x = 0 by METRIC_1:1;
then ( x in cl_Ball x,1 & cl_Ball x,1 = S . n ) by FUNCOP_1:13, METRIC_1:13;
hence not S . y is empty ; :: thesis: verum

end;

now

let i be natural number ; :: thesis: S . i is closed
( i in NAT & ([#] M) \ (cl_Ball x,1) in Family_open_set M ) by NAGATA_1:14, ORDINAL1:def 13;
then ( (cl_Ball x,1) ` is open & S . i = cl_Ball x,1 ) by FUNCOP_1:13, Def3;
hence S . i is closed by Def4; :: thesis: verum

end;

hence ( S is non-empty & S is bounded & S is closed ) by A8, A9, Def1, Def8, FUNCT_1:def 15; :: thesis: verum