let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being real number
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 number
for A being Subset of (TopSpaceMetr M) st A = cl_Ball z,r holds
A ` is open
let r be real number ; :: 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:16;
reconsider Q = Ball e,((dist e,z) - r) as Subset of (TopSpaceMetr M) by TOPMETR:16;
take Q ; :: thesis: ( Q is open & Q c= A ` & x in Q )
thus Q is open by TOPMETR:21; :: thesis: ( Q c= A ` & x in Q )
thus Q c= A ` :: thesis: x in Q

proof

let q be set ; :: 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 ;
A4: dist e,f < (dist e,z) - r by A3, METRIC_1:12;
dist e,z <= (dist e,f) + (dist f,z) by METRIC_1:4;
then (dist e,z) - r <= ((dist e,f) + (dist f,z)) - r by XREAL_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:11;
then 0 < (((dist e,f) - (dist e,f)) + (dist f,z)) - r ;
then dist f,z > r by XREAL_1:49;
then not q in A by A1, METRIC_1:13;
hence q in A ` by A3, SUBSET_1:50; :: thesis: verum

end;

not x in A by A2, XBOOLE_0:def 5;
then dist z,e > r by A1, METRIC_1:13;
then (dist e,z) - r > r - r by XREAL_1:11;
hence x in Q by TBSP_1:16; :: 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:57; :: thesis: verum