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

let x be Point of T; :: thesis:
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))

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

let Z be set ; :: thesis:
assume A7: Z in FHX ; :: thesis:
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:

end;

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:
then x in Cl (union HX) by A5, A8, XBOOLE_0:def 3;
hence x in union (clf FX) by A4, A9; :: thesis:

end;

let x be Point of T; :: thesis:
assume x in union (clf FX) ; :: thesis:
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

end;

end;

end;