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;
set B = Ball (x,1);
take S = NAT --> (Ball (x,1)); :: thesis: ( S is non-empty & S is bounded & S is open )

A2: now

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

end;

A4: now

let i be natural number ; :: thesis: S . i is open
i in NAT by ORDINAL1:def 13;
then A5: S . i = Ball (x,1) by FUNCOP_1:13;
Ball (x,1) in Family_open_set M by PCOMPS_1:33;
hence S . i is open by A5, Def3; :: thesis: verum

end;

now

let i be natural number ; :: thesis: S . i is bounded
i in NAT by ORDINAL1:def 13;
hence S . i is bounded by FUNCOP_1:13; :: thesis: verum

end;

hence ( S is non-empty & S is bounded & S is open ) by A2, A4, Def1, Def7, FUNCT_1:def 15; :: thesis: verum