let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
let FX be Subset-Family of T; :: thesis: ( FX is locally_finite implies clf FX is locally_finite )
set GX = clf FX;
assume A1: FX is locally_finite ; :: thesis: clf FX is locally_finite
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )

proof

let x be Point of T; :: thesis: ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite ) :: thesis: verum

proof

deffunc H₁( Subset of T) -> Element of bool the carrier of T = Cl $1;
consider W being Subset of T such that
A2: x in W and
A3: W is open and
A4: { V where V is Subset of T : ( V in FX & V meets W ) } is finite by A1;
take W ; :: thesis: ( x in W & W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus x in W by A2; :: thesis: ( W is open & { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite )
thus W is open by A3; :: thesis: { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite
set CGX = { V where V is Subset of T : ( V in clf FX & V meets W ) } ;
set CFX = { V where V is Subset of T : ( V in FX & V meets W ) } ;
A5: for Y being Subset of T st Y in FX holds
H₁(Y) in clf FX by Def2;
consider f being Function of FX,(clf FX) such that
A6: for X being Subset of T st X in FX holds
f . X = H₁(X) from PCOMPS_1:sch 1(A5);
A7: ( clf FX = {} implies FX = {} ) by Th17, SETFAM_1:16;
then A8: dom f = FX by FUNCT_2:def 1;
for Z being object holds
( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )

proof

let Z be object ; :: thesis: ( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )
A9: ( Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } implies Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } )

proof

assume A10: Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } ; :: thesis: Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) }
ex Y being set st
( Y in dom f & Y in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . Y )

proof

consider V being Subset of T such that
A11: Z = V and
A12: V in clf FX and
A13: V meets W by A10;
consider X being Subset of T such that
A14: V = Cl X and
A15: X in FX by A12, Def2;
take X ; :: thesis: ( X in dom f & X in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . X )
A16: V /\ W <> {} by A13, XBOOLE_0:def 7;
ex Q being Subset of T st
( X = Q & Q in FX & Q meets W )

proof

take Q = X; :: thesis: ( X = Q & Q in FX & Q meets W )
thus X = Q ; :: thesis: ( Q in FX & Q meets W )
thus Q in FX by A15; :: thesis: Q meets W
Cl (W /\ (Cl Q)) <> {} by A16, A14, Th2;
then Cl (W /\ Q) <> {} by A3, TOPS_1:14;
then Q /\ W <> {} by Th2;
hence Q meets W by XBOOLE_0:def 7; :: thesis: verum

end;

hence ( X in dom f & X in { V where V is Subset of T : ( V in FX & V meets W ) } & Z = f . X ) by A6, A7, A11, A14, FUNCT_2:def 1; :: thesis: verum

end;

hence Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } by FUNCT_1:def 6; :: thesis: verum

end;

( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } implies Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } )

proof

assume Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } ; :: thesis: Z in { V where V is Subset of T : ( V in clf FX & V meets W ) }
then consider Y being object such that
A17: Y in dom f and
A18: Y in { V where V is Subset of T : ( V in FX & V meets W ) } and
A19: Z = f . Y by FUNCT_1:def 6;
reconsider Y = Y as Subset of T by A8, A17;
A20: f . Y = Cl Y by A6, A8, A17;
then reconsider Z = Z as Subset of T by A19;
ex V being Subset of T st
( Y = V & V in FX & V meets W ) by A18;
then A21: Z meets W by A19, A20, PRE_TOPC:18, XBOOLE_1:63;
Z in clf FX by A8, A17, A19, A20, Def2;
hence Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } by A21; :: thesis: verum

end;

hence ( Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } iff Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } ) by A9; :: thesis: verum

end;

hence { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite by A4, TARSKI:2; :: thesis: verum

end;

end;

hence clf FX is locally_finite ; :: thesis: verum