let PT be non empty TopSpace; :: thesis: for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )
let FX be Subset-Family of PT; :: thesis: ( PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open implies ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite ) )
assume that
A1: PT is T_2 and
A2: PT is paracompact and
A3: ( FX is Cover of PT & FX is open ) ; :: thesis: ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )
consider HX being Subset-Family of PT such that
A4: ( HX is open & HX is Cover of PT ) and
A5: for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) by A1, A2, A3, Th2, PCOMPS_1:24;
consider GX being Subset-Family of PT such that
A6: ( GX is open & GX is Cover of PT ) and
A7: GX is_finer_than HX and
A8: GX is locally_finite by A2, A4, PCOMPS_1:def 3;
A9: for V being Subset of PT st V in GX holds
ex W being Subset of PT st
( W in FX & Cl V c= W )

proof

let V be Subset of PT; :: thesis: ( V in GX implies ex W being Subset of PT st
( W in FX & Cl V c= W ) )
assume V in GX ; :: thesis: ex W being Subset of PT st
( W in FX & Cl V c= W )
then consider X being set such that
A10: X in HX and
A11: V c= X by A7;
reconsider X = X as Subset of PT by A10;
consider W being Subset of PT such that
A12: ( W in FX & Cl X c= W ) by A5, A10;
take W ; :: thesis: ( W in FX & Cl V c= W )
Cl V c= Cl X by A11, PRE_TOPC:19;
hence ( W in FX & Cl V c= W ) by A12; :: thesis: verum

end;

clf GX is_finer_than FX

proof

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( not X in clf GX or ex b₁ being set st
( b₁ in FX & X c= b₁ ) )
assume A13: X in clf GX ; :: thesis: ex b₁ being set st
( b₁ in FX & X c= b₁ )
then reconsider X = X as Subset of PT ;
consider V being Subset of PT such that
A14: X = Cl V and
A15: V in GX by A13, PCOMPS_1:def 2;
consider W being Subset of PT such that
A16: ( W in FX & Cl V c= W ) by A9, A15;
take W ; :: thesis: ( W in FX & X c= W )
thus ( W in FX & X c= W ) by A14, A16; :: thesis: verum

end;

hence ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite ) by A6, A8; :: thesis: verum