let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; :: thesis: ( FX is locally_finite implies Cl (union FX) = union (clf FX) )
set UFX = Cl (union FX);
set UCFX = union (clf FX);
assume A1: FX is locally_finite ; :: thesis: Cl (union FX) = union (clf FX)
for x being Point of T st x in Cl (union FX) holds
x in union (clf FX)

proof

let x be Point of T; :: thesis: ( x in Cl (union FX) implies x in union (clf FX) )
consider W being Subset of T such that
A2: ( x in W & W is open ) and
A3: { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A1;
set HX = { V where V is Subset of T : ( V in FX & V meets W ) } ;
reconsider HX = { V where V is Subset of T : ( V in FX & V meets W ) } as Subset-Family of T by Th8, TOPS_2:2;
A4: Cl (union HX) = union (clf HX) by A3, Th16;
set FHX = FX \ HX;
A5: not x in Cl (union (FX \ HX))

proof

assume A6: x in Cl (union (FX \ HX)) ; :: thesis: contradiction
reconsider FHX = FX \ HX as set ;
for Z being set st Z in FHX holds
Z misses W

proof

let Z be set ; :: thesis: ( Z in FHX implies Z misses W )
assume A7: Z in FHX ; :: thesis: Z misses W
then reconsider Z = Z as Subset of T ;
( Z in FX & not Z in HX ) by A7, XBOOLE_0:def 5;
hence Z misses W ; :: thesis: verum

end;

then union FHX misses W by ZFMISC_1:80;
hence contradiction by A2, A6, TOPS_1:12; :: thesis: verum

end;

HX \/ (FX \ HX) = HX \/ FX by XBOOLE_1:39
.= FX by Th8, XBOOLE_1:12 ;
then A8: Cl (union FX) = Cl ((union HX) \/ (union (FX \ HX))) by ZFMISC_1:78
.= (Cl (union HX)) \/ (Cl (union (FX \ HX))) by PRE_TOPC:20 ;
clf HX c= clf FX by Th8, Th14;
then A9: union (clf HX) c= union (clf FX) by ZFMISC_1:77;
assume x in Cl (union FX) ; :: thesis: x in union (clf FX)
then x in Cl (union HX) by A5, A8, XBOOLE_0:def 3;
hence x in union (clf FX) by A4, A9; :: thesis: verum

end;

then A10: Cl (union FX) c= union (clf FX) ;
for x being Point of T st x in union (clf FX) holds
x in Cl (union FX)

proof

let x be Point of T; :: thesis: ( x in union (clf FX) implies x in Cl (union FX) )
assume x in union (clf FX) ; :: thesis: x in Cl (union FX)
then consider X being set such that
A11: x in X and
A12: X in clf FX by TARSKI:def 4;
reconsider X = X as Subset of T by A12;
consider Y being Subset of T such that
A13: X = Cl Y and
A14: Y in FX by A12, Def2;
for A being Subset of T st A is open & x in A holds
union FX meets A

proof

let A be Subset of T; :: thesis: ( A is open & x in A implies union FX meets A )
assume A15: ( A is open & x in A ) ; :: thesis: union FX meets A
ex y being Point of T st y in (union FX) /\ A

proof

Y meets A by A11, A13, A15, TOPS_1:12;
then consider z being object such that
A16: z in Y /\ A by XBOOLE_0:4;
z in Y by A16, XBOOLE_0:def 4;
then A17: z in union FX by A14, TARSKI:def 4;
take z ; :: thesis: ( z is set & z is Point of T & z in (union FX) /\ A )
z in A by A16, XBOOLE_0:def 4;
hence ( z is set & z is Point of T & z in (union FX) /\ A ) by A17, XBOOLE_0:def 4; :: thesis: verum

end;

hence union FX meets A by XBOOLE_0:4; :: thesis: verum

end;

hence x in Cl (union FX) by TOPS_1:12; :: thesis: verum

end;

then union (clf FX) c= Cl (union FX) ;
hence Cl (union FX) = union (clf FX) by A10, XBOOLE_0:def 10; :: thesis: verum