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) )
assume A1: FX is locally_finite ; :: thesis: Cl (union FX) = union (clf FX)
set UFX = Cl (union FX);
set UCFX = union (clf FX);
A2: Cl (union FX) c= union (clf FX)

proof

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) )
assume A3: x in Cl (union FX) ; :: thesis: x in union (clf FX)
consider W being Subset of T such that
A4: x in W and
A5: W is open and
A6: { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A1, Def2;
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 Th11, TOPS_2:3;
set FHX = FX \ HX;
A7: not x in Cl (union (FX \ HX))

proof

assume A8: 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 A9: Z in FHX ; :: thesis: Z misses W
then reconsider Z = Z as Subset of T ;
( Z in FX & not Z in HX ) by A9, XBOOLE_0:def 5;
hence Z misses W ; :: thesis: verum

end;

then union FHX misses W by ZFMISC_1:98;
hence contradiction by A4, A5, A8, TOPS_1:39; :: thesis: verum

end;

HX \/ (FX \ HX) = HX \/ FX by XBOOLE_1:39
.= FX by Th11, XBOOLE_1:12 ;
then Cl (union FX) = Cl ((union HX) \/ (union (FX \ HX))) by ZFMISC_1:96
.= (Cl (union HX)) \/ (Cl (union (FX \ HX))) by PRE_TOPC:50 ;
then A10: x in Cl (union HX) by A3, A7, XBOOLE_0:def 3;
A11: Cl (union HX) = union (clf HX) by A6, Th19;
union (clf HX) c= union (clf FX)

proof

HX c= FX by Th11;
hence union (clf HX) c= union (clf FX) by Th17, ZFMISC_1:95; :: thesis: verum

end;

hence x in union (clf FX) by A10, A11; :: thesis: verum

end;

hence Cl (union FX) c= union (clf FX) by SUBSET_1:7; :: thesis: verum

end;

union (clf FX) c= Cl (union FX)

proof

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
A12: x in X and
A13: X in clf FX by TARSKI:def 4;
reconsider X = X as Subset of T by A13;
consider Y being Subset of T such that
A14: X = Cl Y and
A15: Y in FX by A13, Def3;
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 that
A16: A is open and
A17: 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 A12, A14, A16, A17, TOPS_1:39;
then consider z being set such that
A18: z in Y /\ A by XBOOLE_0:4;
take z ; :: thesis: ( z is Point of T & z in (union FX) /\ A )
A19: ( z in Y & z in A ) by A18, XBOOLE_0:def 4;
then z in union FX by A15, TARSKI:def 4;
hence ( z is Point of T & z in (union FX) /\ A ) by A19, 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:39; :: thesis: verum

end;

hence union (clf FX) c= Cl (union FX) by SUBSET_1:7; :: thesis: verum

end;

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