:: deftheorem defines sigma_discrete NAGATA_1:def 4 :
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is sigma_discrete iff ex f being sigma_discrete FamilySequence of T st F = Union f );