consider x being object 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 pointwise_bounded & S is closed )
A7: now :: thesis: for y being object st y in dom S holds
not S . y is empty
let y be object ; :: 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 ;
A8: cl_Ball (x,1) = S . n by FUNCOP_1:7;
dist (x,x) = 0 by METRIC_1:1;
hence not S . y is empty by A8, METRIC_1:12; :: thesis: verum
end;
A9: now :: thesis: for i being Nat holds S . i is closed
let i be Nat; :: thesis: S . i is closed
i in NAT by ORDINAL1:def 12;
then A10: S . i = cl_Ball (x,1) by FUNCOP_1:7;
([#] M) \ (cl_Ball (x,1)) in Family_open_set M by NAGATA_1:14;
then (cl_Ball (x,1)) ` is open ;
hence S . i is closed by A10; :: thesis: verum
end;
now :: thesis: for i being Nat holds S . i is bounded
let i be Nat; :: thesis: S . i is bounded
A11: i in NAT by ORDINAL1:def 12;
cl_Ball (x,1) is bounded by TOPREAL6:59;
hence S . i is bounded by A11, FUNCOP_1:7; :: thesis: verum
end;
hence ( S is non-empty & S is pointwise_bounded & S is closed ) by A7, A9, FUNCT_1:def 9; :: thesis: verum