let M be 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 )
let V be Subset of (TopSpaceMetr M); ( 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
; 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
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
; ( 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 ) }
; V = union F
reconsider Q = union F as Subset of (TopSpaceMetr M) ;
for z being object holds
( z in V iff z in Q )
hence
V = union F
by TARSKI:2; verum