let T be non empty TopSpace; :: thesis: for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
let FX, GX be Subset-Family of T; :: thesis: ( FX c= GX & GX is locally_finite implies FX is locally_finite )
assume that
A1: FX c= GX and
A2: GX is locally_finite ; :: thesis: FX is locally_finite

now :: thesis: 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 FX & V meets W ) } is finite )

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 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 FX & V meets W ) } is finite ) :: thesis: verum

proof

consider Y being Subset of T such that
A3: x in Y and
A4: Y is open and
A5: { X where X is Subset of T : ( X in GX & X meets Y ) } is finite by A2;
take W = Y; :: thesis: ( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
thus x in W by A3; :: thesis: ( W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite )
thus W is open by A4; :: thesis: { V where V is Subset of T : ( V in FX & V meets W ) } is finite
{ V where V is Subset of T : ( V in FX & V meets W ) } c= { X where X is Subset of T : ( X in GX & X meets Y ) }

proof

let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in { V where V is Subset of T : ( V in FX & V meets W ) } or Z in { X where X is Subset of T : ( X in GX & X meets Y ) } )
assume A6: Z in { V where V is Subset of T : ( V in FX & V meets W ) } ; :: thesis: Z in { X where X is Subset of T : ( X in GX & X meets Y ) }
ex X being Subset of T st
( Z = X & X in GX & X meets Y )

proof

consider V being Subset of T such that
A7: Z = V and
A8: V in FX and
A9: V meets W by A6;
take X = V; :: thesis: ( Z = X & X in GX & X meets Y )
thus Z = X by A7; :: thesis: ( X in GX & X meets Y )
thus X in GX by A1, A8; :: thesis: X meets Y
thus X meets Y by A9; :: thesis: verum

end;

hence Z in { X where X is Subset of T : ( X in GX & X meets Y ) } ; :: thesis: verum

end;

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

end;

end;

hence FX is locally_finite ; :: thesis: verum