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

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)) )

hence
([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM
by PCOMPS_1:def 4; :: thesis: verumex 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))

( 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;( 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
y in ([#] PM) \ (cl_Ball (x,r))
; :: thesis: ex r2 being Real st
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;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

( 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