let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
let FX be Subset-Family of T; :: thesis: ( FX is finite implies FX is locally_finite )
assume A1: FX is finite ; :: thesis: 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 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 FX & V meets W ) } is finite )
take [#] T ; :: thesis: ( x in [#] T & [#] T is open & { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite )
thus x in [#] T ; :: thesis: ( [#] T is open & { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite )
thus [#] T is open ; :: thesis: { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite
thus { V where V is Subset of T : ( V in FX & V meets [#] T ) } is finite by A1, Th8, FINSET_1:1; :: thesis: verum
end;
hence FX is locally_finite ; :: thesis: verum