theorem Th21: :: NAGATA_2:21
for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_discrete