theorem :: NAGATA_1:16

for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite