let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
let FX be Subset-Family of T; :: thesis: ( FX is locally_finite & FX is closed implies union FX is closed )
assume that
A1: FX is locally_finite and
A2: FX is closed ; :: thesis: union FX is closed
union (clf FX) c= union FX

proof

set UFX = union FX;
set UCFX = union (clf FX);
for x being Point of T st x in union (clf FX) holds
x in union FX

proof

let x be Point of T; :: thesis: ( x in union (clf FX) implies x in union FX )
assume x in union (clf FX) ; :: thesis: x in union FX
then consider X being set such that
A3: x in X and
A4: X in clf FX by TARSKI:def 4;
reconsider X = X as Subset of T by A4;
consider W being Subset of T such that
A5: X = Cl W and
A6: W in FX by A4, Def2;
reconsider W = W as Subset of T ;
W is closed by A2, A6, TOPS_2:def 2;
then x in W by A3, A5, PRE_TOPC:22;
hence x in union FX by A6, TARSKI:def 4; :: thesis: verum

end;

hence union (clf FX) c= union FX ; :: thesis: verum

end;

then A7: Cl (union FX) c= union FX by A1, Th20;
union FX c= union (clf FX) by Th17, SETFAM_1:13;
then union FX c= Cl (union FX) by A1, Th20;
hence union FX is closed by A7, XBOOLE_0:def 10; :: thesis: verum