theorem Th11: :: NAGATA_1:11

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
F is locally_finite