theorem :: NAGATA_1:12

for T being non empty TopSpace
for Un being FamilySequence of T st Un is sigma_discrete holds
Un is sigma_locally_finite by Th11;