let T be non empty TopSpace; :: thesis: ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )

now :: thesis: ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete implies T is metrizable )

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

end;

hence ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable ) by Th21, NAGATA_1:15; :: thesis: verum