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 )

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: verumassume 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;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