theorem Th9: :: PCOMPS_1:9

for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite