theorem :: TOPMETR4:3

for M being non empty MetrSpace
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 )