let M be non empty MetrSpace; :: thesis: for V being Subset of (TopSpaceMetr M) st V is open holds
ex F being Subset-Family of M st
( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F )
let V be Subset of (TopSpaceMetr M); :: thesis: ( V is open implies ex F being Subset-Family of M st
( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F ) )
assume A1: V is open ; :: thesis: ex F being Subset-Family of M st
( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F )
set F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } ;
for z being object st z in { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } holds
z in Family_open_set M

proof

let z be object ; :: thesis: ( z in { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } implies z in Family_open_set M )
assume z in { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } ; :: thesis: z in Family_open_set M
then ex x being Element of M ex r being Real st
( z = Ball (x,r) & r > 0 & Ball (x,r) c= V ) ;
hence z in Family_open_set M by PCOMPS_1:29; :: thesis: verum

end;

then { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } c= Family_open_set M by TARSKI:def 3;
then reconsider F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } as Subset-Family of M by XBOOLE_1:1;
take F ; :: thesis: ( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F )
thus F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } ; :: thesis: V = union F
reconsider Q = union F as Subset of (TopSpaceMetr M) ;
for z being object holds
( z in V iff z in Q )

proof

let z be object ; :: thesis: ( z in V iff z in Q )

hereby :: thesis: ( z in Q implies z in V )

assume A2: z in V ; :: thesis: z in Q
then reconsider x = z as Element of M ;
consider r being Real such that
A3: ( r > 0 & Ball (x,r) c= V ) by A1, A2, TOPMETR:15;
dist (x,x) = 0 by METRIC_1:1;
then A4: x in Ball (x,r) by A3, METRIC_1:11;
Ball (x,r) in F by A3;
hence z in Q by A4, TARSKI:def 4; :: thesis: verum

end;

assume z in Q ; :: thesis: z in V
then consider B being set such that
A5: ( z in B & B in F ) by TARSKI:def 4;
consider x being Element of M, r being Real such that
A6: ( B = Ball (x,r) & r > 0 & Ball (x,r) c= V ) by A5;
thus z in V by A5, A6; :: thesis: verum

end;

hence V = union F by TARSKI:2; :: thesis: verum