let V be RealUnitarySpace; :: thesis: 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; :: thesis: ( A c= Family_open_set V implies union A in Family_open_set V )
assume A1:
A c= Family_open_set V
; :: thesis: 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;
:: 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
V by A3;
A4:
W c= union A
by A3, ZFMISC_1:92;
consider r being
Real such that A5:
(
r > 0 &
Ball x,
r c= W )
by A1, A2, A3, Def5;
take
r
;
:: thesis: ( r > 0 & Ball x,r c= union A )
thus
r > 0
by A5;
:: thesis: Ball x,r c= union A
thus
Ball x,
r c= union A
by A4, A5, XBOOLE_1:1;
:: thesis: verum
end;
hence
union A in Family_open_set V
by Def5; :: thesis: verum