let PM be MetrStruct ; :: thesis: for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
let A be Subset-Family of PM; :: thesis: ( A c= Family_open_set PM implies union A in Family_open_set PM )
assume A1: A c= Family_open_set PM ; :: thesis: union A in Family_open_set PM
for x being Element of PM st x in union A holds
ex r being Real st
( r > 0 & Ball (x,r) c= union A )

proof

let x be Element of PM; :: thesis: ( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume x in union A ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= union A )
then consider W being set such that
A2: x in W and
A3: W in A by TARSKI:def 4;
reconsider W = W as Subset of PM by A3;
consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= W by A1, A2, A3, Def4;
take r ; :: thesis: ( r > 0 & Ball (x,r) c= union A )
thus r > 0 by A4; :: thesis: Ball (x,r) c= union A
W c= union A by A3, ZFMISC_1:74;
hence Ball (x,r) c= union A by A5; :: thesis: verum

end;

hence union A in Family_open_set PM by Def4; :: thesis: verum