let r be real number ; :: thesis: for PM being non empty MetrSpace
for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM
reconsider r9 = r as Real by XREAL_0:def 1;
let PM be non empty MetrSpace; :: thesis: for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM
let x be Element of PM; :: thesis: ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM

now

let y be Element of PM; :: thesis: ( y in ([#] PM) \ (cl_Ball (x,r)) implies ex r2 being Real st
( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) )
set r1 = (dist (x,y)) - r9;
A2: Ball (y,((dist (x,y)) - r9)) c= ([#] PM) \ (cl_Ball (x,r))

proof

assume not Ball (y,((dist (x,y)) - r9)) c= ([#] PM) \ (cl_Ball (x,r)) ; :: thesis: contradiction
then consider z being set such that
A3: z in Ball (y,((dist (x,y)) - r9)) and
A4: not z in ([#] PM) \ (cl_Ball (x,r)) by TARSKI:def 3;
reconsider z = z as Element of PM by A3;
( not z in [#] PM or z in cl_Ball (x,r) ) by A4, XBOOLE_0:def 5;
then A5: dist (x,z) <= r9 by METRIC_1:13;
dist (y,z) < (dist (x,y)) - r9 by A3, METRIC_1:12;
then (dist (y,z)) + (dist (x,z)) < ((dist (x,y)) - r9) + r9 by A5, XREAL_1:10;
then (dist (x,z)) + (dist (z,y)) < ((dist (x,y)) - r9) + r9 ;
hence contradiction by METRIC_1:4; :: thesis: verum

end;

assume y in ([#] PM) \ (cl_Ball (x,r)) ; :: thesis: ex r2 being Real st
( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) )
then not y in cl_Ball (x,r) by XBOOLE_0:def 5;
then r9 + 0 < r9 + ((dist (x,y)) - r9) by METRIC_1:13;
then r9 - r9 < ((dist (x,y)) - r9) - 0 by XREAL_1:23;
hence ex r2 being Real st
( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) by A2; :: thesis: verum

end;

hence ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM by PCOMPS_1:def 5; :: thesis: verum