let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being Real
for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A ` is open
let z be Point of M; :: thesis: for r being Real
for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A ` is open
let r be Real; :: thesis: for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A ` is open
let A be Subset of (TopSpaceMetr M); :: thesis: ( A = cl_Ball (z,r) implies A ` is open )
assume A1: A = cl_Ball (z,r) ; :: thesis: A ` is open
for x being set holds
( x in A ` iff ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q ) )

proof

let x be set ; :: thesis: ( x in A ` iff ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q ) )
thus ( x in A ` implies ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q ) ) :: thesis: ( ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q ) implies x in A ` )

proof

assume A2: x in A ` ; :: thesis: ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q )
then reconsider e = x as Point of M by TOPMETR:12;
reconsider Q = Ball (e,((dist (e,z)) - r)) as Subset of (TopSpaceMetr M) by TOPMETR:12;
take Q ; :: thesis: ( Q is open & Q c= A ` & x in Q )
thus Q is open by TOPMETR:14; :: thesis: ( Q c= A ` & x in Q )
thus Q c= A ` :: thesis: x in Q

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Q or q in A ` )
assume A3: q in Q ; :: thesis: q in A `
then reconsider f = q as Point of M ;
dist (e,z) <= (dist (e,f)) + (dist (f,z)) by METRIC_1:4;
then A4: (dist (e,z)) - r <= ((dist (e,f)) + (dist (f,z))) - r by XREAL_1:9;
dist (e,f) < (dist (e,z)) - r by A3, METRIC_1:11;
then dist (e,f) < ((dist (e,f)) + (dist (f,z))) - r by A4, XXREAL_0:2;
then (dist (e,f)) - (dist (e,f)) < (((dist (e,f)) + (dist (f,z))) - r) - (dist (e,f)) by XREAL_1:9;
then 0 < (((dist (e,f)) - (dist (e,f))) + (dist (f,z))) - r ;
then dist (f,z) > r by XREAL_1:47;
then not q in A by A1, METRIC_1:12;
hence q in A ` by A3, SUBSET_1:29; :: thesis: verum

end;

not x in A by A2, XBOOLE_0:def 5;
then dist (z,e) > r by A1, METRIC_1:12;
then (dist (e,z)) - r > r - r by XREAL_1:9;
hence x in Q by TBSP_1:11; :: thesis: verum

end;

thus ( ex Q being Subset of (TopSpaceMetr M) st
( Q is open & Q c= A ` & x in Q ) implies x in A ` ) ; :: thesis: verum

end;

hence A ` is open by TOPS_1:25; :: thesis: verum