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;
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 PM
by Def5; :: thesis: verum