assume that
A1: ( T is regular & T is T_1 ) and
A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ; :: thesis: T is metrizable
consider Bn being FamilySequence of T such that
A3: Bn is Basis_sigma_discrete by A2;
Bn is sigma_discrete by A3, NAGATA_1:def 5;
then A4: Bn is sigma_locally_finite by NAGATA_1:12;
Union Bn is Basis of T by A3, NAGATA_1:def 5;
then Bn is Basis_sigma_locally_finite by A4, NAGATA_1:def 6;
hence T is metrizable by A1, Th19; :: thesis: verum