let r be Real; :: 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 ;
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 :: thesis: for y being Element of PM st y in ([#] PM) \ (cl_Ball (x,r)) holds
ex r2 being Real st
( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) )
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;
A1: 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 object such that
A2: z in Ball (y,((dist (x,y)) - r9)) and
A3: not z in ([#] PM) \ (cl_Ball (x,r)) ;
reconsider z = z as Element of PM by A2;
( not z in [#] PM or z in cl_Ball (x,r) ) by A3, XBOOLE_0:def 5;
then A4: dist (x,z) <= r9 by METRIC_1:12;
dist (y,z) < (dist (x,y)) - r9 by A2, METRIC_1:11;
then (dist (y,z)) + (dist (x,z)) < ((dist (x,y)) - r9) + r9 by A4, XREAL_1:8;
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:12;
then r9 - r9 < ((dist (x,y)) - r9) - 0 by XREAL_1:21;
hence ex r2 being Real st
( r2 > 0 & Ball (y,r2) c= ([#] PM) \ (cl_Ball (x,r)) ) by A1; :: thesis: verum
end;
hence ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM by PCOMPS_1:def 4; :: thesis: verum