let M be non empty MetrSpace; :: thesis:
let V be Subset of (TopSpaceMetr M); :: thesis:
assume A1: V is open ; :: thesis:
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

let z be object ; :: thesis:
assume z in { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } ; :: thesis:
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:

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:
thus F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } ; :: thesis:
reconsider Q = union F as Subset of (TopSpaceMetr M) ;
for z being object holds
( z in V iff z in Q )

let z be object ; :: thesis:

assume A2: z in V ; :: thesis:
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:

end;

assume z in Q ; :: thesis:
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:

end;