:: deftheorem defines Basis_sigma_locally_finite NAGATA_1:def 6 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is Basis_sigma_locally_finite iff ( Un is sigma_locally_finite & Union Un is Basis of T ) );