let PM be MetrStruct ; 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; ( A c= Family_open_set PM implies union A in Family_open_set PM )
assume A1:
A c= Family_open_set PM
; 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;
( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume
x in union A
;
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
;
( r > 0 & Ball (x,r) c= union A )
thus
r > 0
by A4;
Ball (x,r) c= union A
W c= union A
by A3, ZFMISC_1:74;
hence
Ball (
x,
r)
c= union A
by A5;
verum
end;
hence
union A in Family_open_set PM
by Def4; verum