let V be RealUnitarySpace; for A being Subset-Family of V st A c= Family_open_set V holds
union A in Family_open_set V
let A be Subset-Family of V; ( A c= Family_open_set V implies union A in Family_open_set V )
assume A1:
A c= Family_open_set V
; union A in Family_open_set V
for x being Point of V st x in union A holds
ex r being Real st
( r > 0 & Ball (x,r) c= union A )
proof
let x be
Point of
V;
( 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
V by A3;
consider r being
Real such that A4:
r > 0
and A5:
Ball (
x,
r)
c= W
by A1, A2, A3, Def5;
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 V
by Def5; verum