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 )
assume A1: FX is locally_finite ; :: thesis: clf FX is locally_finite
set GX = clf FX;
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

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, Def2;
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 ) } ;
deffunc H₁( Subset of T) -> Element of bool the carrier of T = Cl $1;
A5: for Y being Subset of T st Y in FX holds
H₁(Y) in clf FX by Def3;
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: dom f = FX

proof

( clf FX = {} implies FX = {} ) by Th20, SETFAM_1:21;
hence dom f = FX by FUNCT_2:def 1; :: thesis: verum

end;

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

proof

for Z being set 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 set ; :: 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 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 set such that
A10: Y in dom f and
A11: Y in { V where V is Subset of T : ( V in FX & V meets W ) } and
A12: Z = f . Y by FUNCT_1:def 12;
reconsider Y = Y as Subset of T by A7, A10;
A13: f . Y = Cl Y by A6, A7, A10;
then reconsider Z = Z as Subset of T by A12;
A14: Z in clf FX by A7, A10, A12, A13, Def3;
consider V being Subset of T such that
A15: Y = V and
V in FX and
A16: V meets W by A11;
Z meets W by A12, A13, A15, A16, PRE_TOPC:48, XBOOLE_1:63;
hence Z in { V where V is Subset of T : ( V in clf FX & V meets W ) } by A14; :: thesis: verum

end;

( 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 A17: 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
A18: Z = V and
A19: V in clf FX and
A20: V meets W by A17;
A21: V /\ W <> {} by A20, XBOOLE_0:def 7;
consider X being Subset of T such that
A22: V = Cl X and
A23: X in FX by A19, Def3;
A24: X in { V where V is Subset of T : ( V in FX & V meets W ) }

proof

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 A23; :: thesis: Q meets W
Cl (W /\ (Cl Q)) <> {} by A21, A22, Th2;
then Cl (W /\ Q) <> {} by A3, TOPS_1:41;
then Q /\ W <> {} by Th2;
hence Q meets W by XBOOLE_0:def 7; :: thesis: verum

end;

hence X in { V where V is Subset of T : ( V in FX & V meets W ) } ; :: thesis: verum

end;

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 )
thus ( 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, A18, A22, A23, A24; :: thesis: verum

end;

hence Z in f .: { V where V is Subset of T : ( V in FX & V meets W ) } by FUNCT_1:def 12; :: 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 f .: { V where V is Subset of T : ( V in FX & V meets W ) } = { V where V is Subset of T : ( V in clf FX & V meets W ) } by TARSKI:2; :: thesis: verum

end;

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
thus { V where V is Subset of T : ( V in clf FX & V meets W ) } is finite by A4, A8; :: thesis: verum

end;

end;

hence clf FX is locally_finite by Def2; :: thesis: verum