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