:: deftheorem Def2 defines sigma_discrete NAGATA_1:def 2 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is sigma_discrete iff for n being Element of NAT holds Un . n is discrete );